
(set-option :produce-models true)
(set-logic QF_ABV)
(declare-fun memory0 () (Array (_ BitVec 32) (_ BitVec 8)))
(declare-fun eax0 () (_ BitVec 32))
(declare-fun ebx0 () (_ BitVec 32))
(declare-fun ecx0 () (_ BitVec 32))
(declare-fun edx0 () (_ BitVec 32))
(declare-fun esi0 () (_ BitVec 32))
(declare-fun edi0 () (_ BitVec 32))
(declare-fun ebp0 () (_ BitVec 32))
(declare-fun esp0 () (_ BitVec 32))
(declare-fun OF0 () (_ BitVec 1))
(declare-fun SF0 () (_ BitVec 1))
(declare-fun ZF0 () (_ BitVec 1))
(declare-fun PF0 () (_ BitVec 1))
(declare-fun CF0 () (_ BitVec 1))
(declare-fun AF0 () (_ BitVec 1))
(declare-fun DF0 () (_ BitVec 1))
(declare-fun fs_base0 () (_ BitVec 32))
(define-fun temp320 () (_ BitVec 32) esp0)
(define-fun memory1 () (Array (_ BitVec 32) (_ BitVec 8)) (store (store (store (store memory0 (bvsub esp0 (_ bv4 32)) ((_ extract 7 0) eax0)) (bvsub esp0 (_ bv3 32)) ((_ extract 15 8) eax0)) (bvsub esp0 (_ bv2 32)) ((_ extract 23 16) eax0)) (bvsub esp0 (_ bv1 32)) ((_ extract 31 24) eax0)))
(define-fun esp1 () (_ BitVec 32) (bvsub esp0 (_ bv4 32)))
(define-fun memory2 () (Array (_ BitVec 32) (_ BitVec 8)) (store (store (store (store memory1 (bvsub esp1 (_ bv4 32)) ((_ extract 7 0) ecx0)) (bvsub esp1 (_ bv3 32)) ((_ extract 15 8) ecx0)) (bvsub esp1 (_ bv2 32)) ((_ extract 23 16) ecx0)) (bvsub esp1 (_ bv1 32)) ((_ extract 31 24) ecx0)))
(define-fun esp2 () (_ BitVec 32) (bvsub esp1 (_ bv4 32)))
(define-fun memory3 () (Array (_ BitVec 32) (_ BitVec 8)) (store (store (store (store memory2 (bvsub esp2 (_ bv4 32)) ((_ extract 7 0) edx0)) (bvsub esp2 (_ bv3 32)) ((_ extract 15 8) edx0)) (bvsub esp2 (_ bv2 32)) ((_ extract 23 16) edx0)) (bvsub esp2 (_ bv1 32)) ((_ extract 31 24) edx0)))
(define-fun esp3 () (_ BitVec 32) (bvsub esp2 (_ bv4 32)))
(define-fun memory4 () (Array (_ BitVec 32) (_ BitVec 8)) (store (store (store (store memory3 (bvsub esp3 (_ bv4 32)) ((_ extract 7 0) ebx0)) (bvsub esp3 (_ bv3 32)) ((_ extract 15 8) ebx0)) (bvsub esp3 (_ bv2 32)) ((_ extract 23 16) ebx0)) (bvsub esp3 (_ bv1 32)) ((_ extract 31 24) ebx0)))
(define-fun esp4 () (_ BitVec 32) (bvsub esp3 (_ bv4 32)))
(define-fun memory5 () (Array (_ BitVec 32) (_ BitVec 8)) (store (store (store (store memory4 (bvsub esp4 (_ bv4 32)) ((_ extract 7 0) temp320)) (bvsub esp4 (_ bv3 32)) ((_ extract 15 8) temp320)) (bvsub esp4 (_ bv2 32)) ((_ extract 23 16) temp320)) (bvsub esp4 (_ bv1 32)) ((_ extract 31 24) temp320)))
(define-fun esp5 () (_ BitVec 32) (bvsub esp4 (_ bv4 32)))
(define-fun memory6 () (Array (_ BitVec 32) (_ BitVec 8)) (store (store (store (store memory5 (bvsub esp5 (_ bv4 32)) ((_ extract 7 0) ebp0)) (bvsub esp5 (_ bv3 32)) ((_ extract 15 8) ebp0)) (bvsub esp5 (_ bv2 32)) ((_ extract 23 16) ebp0)) (bvsub esp5 (_ bv1 32)) ((_ extract 31 24) ebp0)))
(define-fun esp6 () (_ BitVec 32) (bvsub esp5 (_ bv4 32)))
(define-fun memory7 () (Array (_ BitVec 32) (_ BitVec 8)) (store (store (store (store memory6 (bvsub esp6 (_ bv4 32)) ((_ extract 7 0) esi0)) (bvsub esp6 (_ bv3 32)) ((_ extract 15 8) esi0)) (bvsub esp6 (_ bv2 32)) ((_ extract 23 16) esi0)) (bvsub esp6 (_ bv1 32)) ((_ extract 31 24) esi0)))
(define-fun esp7 () (_ BitVec 32) (bvsub esp6 (_ bv4 32)))
(define-fun memory8 () (Array (_ BitVec 32) (_ BitVec 8)) (store (store (store (store memory7 (bvsub esp7 (_ bv4 32)) ((_ extract 7 0) edi0)) (bvsub esp7 (_ bv3 32)) ((_ extract 15 8) edi0)) (bvsub esp7 (_ bv2 32)) ((_ extract 23 16) edi0)) (bvsub esp7 (_ bv1 32)) ((_ extract 31 24) edi0)))
(define-fun esp8 () (_ BitVec 32) (bvsub esp7 (_ bv4 32)))
(define-fun esp9 () (_ BitVec 32) (bvsub esp8 (_ bv4 32)))
(define-fun memory9 () (Array (_ BitVec 32) (_ BitVec 8)) (store (store (store (store memory8 esp9 (_ bv7 8)) (bvadd esp9 (_ bv1 32)) (_ bv80 8)) (bvadd esp9 (_ bv2 32)) (_ bv0 8)) (bvadd esp9 (_ bv3 32)) (_ bv1 8)))
(assert (= eax0 (_ bv0 32)))
(assert (= ebx0 (_ bv0 32)))
(assert (= ecx0 (_ bv0 32)))
(assert (= edx0 (_ bv0 32)))
(assert (= edi0 (_ bv0 32)))
(assert (= esi0 (_ bv0 32)))
(assert (= esp0 (_ bv458752 32)))
(assert (= ebp0 (_ bv458752 32)))
(check-sat)
(reset)



(set-option :produce-models true)
(set-logic QF_ABV)
(declare-fun memory0 () (Array (_ BitVec 32) (_ BitVec 8)))
(declare-fun eax0 () (_ BitVec 32))
(declare-fun ebx0 () (_ BitVec 32))
(declare-fun ecx0 () (_ BitVec 32))
(declare-fun edx0 () (_ BitVec 32))
(declare-fun esi0 () (_ BitVec 32))
(declare-fun edi0 () (_ BitVec 32))
(declare-fun ebp0 () (_ BitVec 32))
(declare-fun esp0 () (_ BitVec 32))
(declare-fun OF0 () (_ BitVec 1))
(declare-fun SF0 () (_ BitVec 1))
(declare-fun ZF0 () (_ BitVec 1))
(declare-fun PF0 () (_ BitVec 1))
(declare-fun CF0 () (_ BitVec 1))
(declare-fun AF0 () (_ BitVec 1))
(declare-fun DF0 () (_ BitVec 1))
(declare-fun fs_base0 () (_ BitVec 32))
(define-fun temp320 () (_ BitVec 32) esp0)
(define-fun memory1 () (Array (_ BitVec 32) (_ BitVec 8)) (store (store (store (store memory0 (bvsub esp0 (_ bv4 32)) ((_ extract 7 0) eax0)) (bvsub esp0 (_ bv3 32)) ((_ extract 15 8) eax0)) (bvsub esp0 (_ bv2 32)) ((_ extract 23 16) eax0)) (bvsub esp0 (_ bv1 32)) ((_ extract 31 24) eax0)))
(define-fun esp1 () (_ BitVec 32) (bvsub esp0 (_ bv4 32)))
(define-fun memory2 () (Array (_ BitVec 32) (_ BitVec 8)) (store (store (store (store memory1 (bvsub esp1 (_ bv4 32)) ((_ extract 7 0) ecx0)) (bvsub esp1 (_ bv3 32)) ((_ extract 15 8) ecx0)) (bvsub esp1 (_ bv2 32)) ((_ extract 23 16) ecx0)) (bvsub esp1 (_ bv1 32)) ((_ extract 31 24) ecx0)))
(define-fun esp2 () (_ BitVec 32) (bvsub esp1 (_ bv4 32)))
(define-fun memory3 () (Array (_ BitVec 32) (_ BitVec 8)) (store (store (store (store memory2 (bvsub esp2 (_ bv4 32)) ((_ extract 7 0) edx0)) (bvsub esp2 (_ bv3 32)) ((_ extract 15 8) edx0)) (bvsub esp2 (_ bv2 32)) ((_ extract 23 16) edx0)) (bvsub esp2 (_ bv1 32)) ((_ extract 31 24) edx0)))
(define-fun esp3 () (_ BitVec 32) (bvsub esp2 (_ bv4 32)))
(define-fun memory4 () (Array (_ BitVec 32) (_ BitVec 8)) (store (store (store (store memory3 (bvsub esp3 (_ bv4 32)) ((_ extract 7 0) ebx0)) (bvsub esp3 (_ bv3 32)) ((_ extract 15 8) ebx0)) (bvsub esp3 (_ bv2 32)) ((_ extract 23 16) ebx0)) (bvsub esp3 (_ bv1 32)) ((_ extract 31 24) ebx0)))
(define-fun esp4 () (_ BitVec 32) (bvsub esp3 (_ bv4 32)))
(define-fun memory5 () (Array (_ BitVec 32) (_ BitVec 8)) (store (store (store (store memory4 (bvsub esp4 (_ bv4 32)) ((_ extract 7 0) temp320)) (bvsub esp4 (_ bv3 32)) ((_ extract 15 8) temp320)) (bvsub esp4 (_ bv2 32)) ((_ extract 23 16) temp320)) (bvsub esp4 (_ bv1 32)) ((_ extract 31 24) temp320)))
(define-fun esp5 () (_ BitVec 32) (bvsub esp4 (_ bv4 32)))
(define-fun memory6 () (Array (_ BitVec 32) (_ BitVec 8)) (store (store (store (store memory5 (bvsub esp5 (_ bv4 32)) ((_ extract 7 0) ebp0)) (bvsub esp5 (_ bv3 32)) ((_ extract 15 8) ebp0)) (bvsub esp5 (_ bv2 32)) ((_ extract 23 16) ebp0)) (bvsub esp5 (_ bv1 32)) ((_ extract 31 24) ebp0)))
(define-fun esp6 () (_ BitVec 32) (bvsub esp5 (_ bv4 32)))
(define-fun memory7 () (Array (_ BitVec 32) (_ BitVec 8)) (store (store (store (store memory6 (bvsub esp6 (_ bv4 32)) ((_ extract 7 0) esi0)) (bvsub esp6 (_ bv3 32)) ((_ extract 15 8) esi0)) (bvsub esp6 (_ bv2 32)) ((_ extract 23 16) esi0)) (bvsub esp6 (_ bv1 32)) ((_ extract 31 24) esi0)))
(define-fun esp7 () (_ BitVec 32) (bvsub esp6 (_ bv4 32)))
(define-fun memory8 () (Array (_ BitVec 32) (_ BitVec 8)) (store (store (store (store memory7 (bvsub esp7 (_ bv4 32)) ((_ extract 7 0) edi0)) (bvsub esp7 (_ bv3 32)) ((_ extract 15 8) edi0)) (bvsub esp7 (_ bv2 32)) ((_ extract 23 16) edi0)) (bvsub esp7 (_ bv1 32)) ((_ extract 31 24) edi0)))
(define-fun esp8 () (_ BitVec 32) (bvsub esp7 (_ bv4 32)))
(define-fun esp9 () (_ BitVec 32) (bvsub esp8 (_ bv4 32)))
(define-fun memory9 () (Array (_ BitVec 32) (_ BitVec 8)) (store (store (store (store memory8 esp9 (_ bv7 8)) (bvadd esp9 (_ bv1 32)) (_ bv80 8)) (bvadd esp9 (_ bv2 32)) (_ bv0 8)) (bvadd esp9 (_ bv3 32)) (_ bv1 8)))
(assert (= eax0 (_ bv0 32)))
(assert (= ebx0 (_ bv0 32)))
(assert (= ecx0 (_ bv0 32)))
(assert (= edx0 (_ bv0 32)))
(assert (= edi0 (_ bv0 32)))
(assert (= esi0 (_ bv0 32)))
(assert (= esp0 (_ bv458752 32)))
(assert (= ebp0 (_ bv458752 32)))
(check-sat)
(reset)




(set-option :produce-models true)
(set-logic QF_ABV)
(declare-fun memory0 () (Array (_ BitVec 32) (_ BitVec 8)))
(declare-fun eax0 () (_ BitVec 32))
(declare-fun ebx0 () (_ BitVec 32))
(declare-fun ecx0 () (_ BitVec 32))
(declare-fun edx0 () (_ BitVec 32))
(declare-fun esi0 () (_ BitVec 32))
(declare-fun edi0 () (_ BitVec 32))
(declare-fun ebp0 () (_ BitVec 32))
(declare-fun esp0 () (_ BitVec 32))
(declare-fun OF0 () (_ BitVec 1))
(declare-fun SF0 () (_ BitVec 1))
(declare-fun ZF0 () (_ BitVec 1))
(declare-fun PF0 () (_ BitVec 1))
(declare-fun CF0 () (_ BitVec 1))
(declare-fun AF0 () (_ BitVec 1))
(declare-fun DF0 () (_ BitVec 1))
(declare-fun fs_base0 () (_ BitVec 32))
(define-fun temp320 () (_ BitVec 32) esp0)
(define-fun memory1 () (Array (_ BitVec 32) (_ BitVec 8)) (store (store (store (store memory0 (bvsub esp0 (_ bv4 32)) ((_ extract 7 0) eax0)) (bvsub esp0 (_ bv3 32)) ((_ extract 15 8) eax0)) (bvsub esp0 (_ bv2 32)) ((_ extract 23 16) eax0)) (bvsub esp0 (_ bv1 32)) ((_ extract 31 24) eax0)))
(define-fun esp1 () (_ BitVec 32) (bvsub esp0 (_ bv4 32)))
(define-fun memory2 () (Array (_ BitVec 32) (_ BitVec 8)) (store (store (store (store memory1 (bvsub esp1 (_ bv4 32)) ((_ extract 7 0) ecx0)) (bvsub esp1 (_ bv3 32)) ((_ extract 15 8) ecx0)) (bvsub esp1 (_ bv2 32)) ((_ extract 23 16) ecx0)) (bvsub esp1 (_ bv1 32)) ((_ extract 31 24) ecx0)))
(define-fun esp2 () (_ BitVec 32) (bvsub esp1 (_ bv4 32)))
(define-fun memory3 () (Array (_ BitVec 32) (_ BitVec 8)) (store (store (store (store memory2 (bvsub esp2 (_ bv4 32)) ((_ extract 7 0) edx0)) (bvsub esp2 (_ bv3 32)) ((_ extract 15 8) edx0)) (bvsub esp2 (_ bv2 32)) ((_ extract 23 16) edx0)) (bvsub esp2 (_ bv1 32)) ((_ extract 31 24) edx0)))
(define-fun esp3 () (_ BitVec 32) (bvsub esp2 (_ bv4 32)))
(define-fun memory4 () (Array (_ BitVec 32) (_ BitVec 8)) (store (store (store (store memory3 (bvsub esp3 (_ bv4 32)) ((_ extract 7 0) ebx0)) (bvsub esp3 (_ bv3 32)) ((_ extract 15 8) ebx0)) (bvsub esp3 (_ bv2 32)) ((_ extract 23 16) ebx0)) (bvsub esp3 (_ bv1 32)) ((_ extract 31 24) ebx0)))
(define-fun esp4 () (_ BitVec 32) (bvsub esp3 (_ bv4 32)))
(define-fun memory5 () (Array (_ BitVec 32) (_ BitVec 8)) (store (store (store (store memory4 (bvsub esp4 (_ bv4 32)) ((_ extract 7 0) temp320)) (bvsub esp4 (_ bv3 32)) ((_ extract 15 8) temp320)) (bvsub esp4 (_ bv2 32)) ((_ extract 23 16) temp320)) (bvsub esp4 (_ bv1 32)) ((_ extract 31 24) temp320)))
(define-fun esp5 () (_ BitVec 32) (bvsub esp4 (_ bv4 32)))
(define-fun memory6 () (Array (_ BitVec 32) (_ BitVec 8)) (store (store (store (store memory5 (bvsub esp5 (_ bv4 32)) ((_ extract 7 0) ebp0)) (bvsub esp5 (_ bv3 32)) ((_ extract 15 8) ebp0)) (bvsub esp5 (_ bv2 32)) ((_ extract 23 16) ebp0)) (bvsub esp5 (_ bv1 32)) ((_ extract 31 24) ebp0)))
(define-fun esp6 () (_ BitVec 32) (bvsub esp5 (_ bv4 32)))
(define-fun memory7 () (Array (_ BitVec 32) (_ BitVec 8)) (store (store (store (store memory6 (bvsub esp6 (_ bv4 32)) ((_ extract 7 0) esi0)) (bvsub esp6 (_ bv3 32)) ((_ extract 15 8) esi0)) (bvsub esp6 (_ bv2 32)) ((_ extract 23 16) esi0)) (bvsub esp6 (_ bv1 32)) ((_ extract 31 24) esi0)))
(define-fun esp7 () (_ BitVec 32) (bvsub esp6 (_ bv4 32)))
(define-fun memory8 () (Array (_ BitVec 32) (_ BitVec 8)) (store (store (store (store memory7 (bvsub esp7 (_ bv4 32)) ((_ extract 7 0) edi0)) (bvsub esp7 (_ bv3 32)) ((_ extract 15 8) edi0)) (bvsub esp7 (_ bv2 32)) ((_ extract 23 16) edi0)) (bvsub esp7 (_ bv1 32)) ((_ extract 31 24) edi0)))
(define-fun esp8 () (_ BitVec 32) (bvsub esp7 (_ bv4 32)))
(define-fun esp9 () (_ BitVec 32) (bvsub esp8 (_ bv4 32)))
(define-fun memory9 () (Array (_ BitVec 32) (_ BitVec 8)) (store (store (store (store memory8 esp9 (_ bv7 8)) (bvadd esp9 (_ bv1 32)) (_ bv80 8)) (bvadd esp9 (_ bv2 32)) (_ bv0 8)) (bvadd esp9 (_ bv3 32)) (_ bv1 8)))
(assert (= eax0 (_ bv0 32)))
(assert (= ebx0 (_ bv0 32)))
(assert (= ecx0 (_ bv0 32)))
(assert (= edx0 (_ bv0 32)))
(assert (= edi0 (_ bv0 32)))
(assert (= esi0 (_ bv0 32)))
(assert (= esp0 (_ bv458752 32)))
(assert (= ebp0 (_ bv458752 32)))
(check-sat)
(reset)




(set-option :produce-models true)
(set-logic QF_ABV)
(declare-fun memory0 () (Array (_ BitVec 32) (_ BitVec 8)))
(declare-fun eax0 () (_ BitVec 32))
(declare-fun ebx0 () (_ BitVec 32))
(declare-fun ecx0 () (_ BitVec 32))
(declare-fun edx0 () (_ BitVec 32))
(declare-fun esi0 () (_ BitVec 32))
(declare-fun edi0 () (_ BitVec 32))
(declare-fun ebp0 () (_ BitVec 32))
(declare-fun esp0 () (_ BitVec 32))
(declare-fun OF0 () (_ BitVec 1))
(declare-fun SF0 () (_ BitVec 1))
(declare-fun ZF0 () (_ BitVec 1))
(declare-fun PF0 () (_ BitVec 1))
(declare-fun CF0 () (_ BitVec 1))
(declare-fun AF0 () (_ BitVec 1))
(declare-fun DF0 () (_ BitVec 1))
(declare-fun fs_base0 () (_ BitVec 32))
(define-fun temp320 () (_ BitVec 32) esp0)
(define-fun memory1 () (Array (_ BitVec 32) (_ BitVec 8)) (store (store (store (store memory0 (bvsub esp0 (_ bv4 32)) ((_ extract 7 0) eax0)) (bvsub esp0 (_ bv3 32)) ((_ extract 15 8) eax0)) (bvsub esp0 (_ bv2 32)) ((_ extract 23 16) eax0)) (bvsub esp0 (_ bv1 32)) ((_ extract 31 24) eax0)))
(define-fun esp1 () (_ BitVec 32) (bvsub esp0 (_ bv4 32)))
(define-fun memory2 () (Array (_ BitVec 32) (_ BitVec 8)) (store (store (store (store memory1 (bvsub esp1 (_ bv4 32)) ((_ extract 7 0) ecx0)) (bvsub esp1 (_ bv3 32)) ((_ extract 15 8) ecx0)) (bvsub esp1 (_ bv2 32)) ((_ extract 23 16) ecx0)) (bvsub esp1 (_ bv1 32)) ((_ extract 31 24) ecx0)))
(define-fun esp2 () (_ BitVec 32) (bvsub esp1 (_ bv4 32)))
(define-fun memory3 () (Array (_ BitVec 32) (_ BitVec 8)) (store (store (store (store memory2 (bvsub esp2 (_ bv4 32)) ((_ extract 7 0) edx0)) (bvsub esp2 (_ bv3 32)) ((_ extract 15 8) edx0)) (bvsub esp2 (_ bv2 32)) ((_ extract 23 16) edx0)) (bvsub esp2 (_ bv1 32)) ((_ extract 31 24) edx0)))
(define-fun esp3 () (_ BitVec 32) (bvsub esp2 (_ bv4 32)))
(define-fun memory4 () (Array (_ BitVec 32) (_ BitVec 8)) (store (store (store (store memory3 (bvsub esp3 (_ bv4 32)) ((_ extract 7 0) ebx0)) (bvsub esp3 (_ bv3 32)) ((_ extract 15 8) ebx0)) (bvsub esp3 (_ bv2 32)) ((_ extract 23 16) ebx0)) (bvsub esp3 (_ bv1 32)) ((_ extract 31 24) ebx0)))
(define-fun esp4 () (_ BitVec 32) (bvsub esp3 (_ bv4 32)))
(define-fun memory5 () (Array (_ BitVec 32) (_ BitVec 8)) (store (store (store (store memory4 (bvsub esp4 (_ bv4 32)) ((_ extract 7 0) temp320)) (bvsub esp4 (_ bv3 32)) ((_ extract 15 8) temp320)) (bvsub esp4 (_ bv2 32)) ((_ extract 23 16) temp320)) (bvsub esp4 (_ bv1 32)) ((_ extract 31 24) temp320)))
(define-fun esp5 () (_ BitVec 32) (bvsub esp4 (_ bv4 32)))
(define-fun memory6 () (Array (_ BitVec 32) (_ BitVec 8)) (store (store (store (store memory5 (bvsub esp5 (_ bv4 32)) ((_ extract 7 0) ebp0)) (bvsub esp5 (_ bv3 32)) ((_ extract 15 8) ebp0)) (bvsub esp5 (_ bv2 32)) ((_ extract 23 16) ebp0)) (bvsub esp5 (_ bv1 32)) ((_ extract 31 24) ebp0)))
(define-fun esp6 () (_ BitVec 32) (bvsub esp5 (_ bv4 32)))
(define-fun memory7 () (Array (_ BitVec 32) (_ BitVec 8)) (store (store (store (store memory6 (bvsub esp6 (_ bv4 32)) ((_ extract 7 0) esi0)) (bvsub esp6 (_ bv3 32)) ((_ extract 15 8) esi0)) (bvsub esp6 (_ bv2 32)) ((_ extract 23 16) esi0)) (bvsub esp6 (_ bv1 32)) ((_ extract 31 24) esi0)))
(define-fun esp7 () (_ BitVec 32) (bvsub esp6 (_ bv4 32)))
(define-fun memory8 () (Array (_ BitVec 32) (_ BitVec 8)) (store (store (store (store memory7 (bvsub esp7 (_ bv4 32)) ((_ extract 7 0) edi0)) (bvsub esp7 (_ bv3 32)) ((_ extract 15 8) edi0)) (bvsub esp7 (_ bv2 32)) ((_ extract 23 16) edi0)) (bvsub esp7 (_ bv1 32)) ((_ extract 31 24) edi0)))
(define-fun esp8 () (_ BitVec 32) (bvsub esp7 (_ bv4 32)))
(define-fun esp9 () (_ BitVec 32) (bvsub esp8 (_ bv4 32)))
(define-fun memory9 () (Array (_ BitVec 32) (_ BitVec 8)) (store (store (store (store memory8 esp9 (_ bv7 8)) (bvadd esp9 (_ bv1 32)) (_ bv80 8)) (bvadd esp9 (_ bv2 32)) (_ bv0 8)) (bvadd esp9 (_ bv3 32)) (_ bv1 8)))
(assert (= eax0 (_ bv0 32)))
(assert (= ebx0 (_ bv0 32)))
(assert (= ecx0 (_ bv0 32)))
(assert (= edx0 (_ bv0 32)))
(assert (= edi0 (_ bv0 32)))
(assert (= esi0 (_ bv0 32)))
(assert (= esp0 (_ bv458752 32)))
(assert (= ebp0 (_ bv458752 32)))
(check-sat)
(reset)




(set-option :produce-models true)
(set-logic QF_ABV)
(declare-fun memory0 () (Array (_ BitVec 32) (_ BitVec 8)))
(declare-fun eax0 () (_ BitVec 32))
(declare-fun ebx0 () (_ BitVec 32))
(declare-fun ecx0 () (_ BitVec 32))
(declare-fun edx0 () (_ BitVec 32))
(declare-fun esi0 () (_ BitVec 32))
(declare-fun edi0 () (_ BitVec 32))
(declare-fun ebp0 () (_ BitVec 32))
(declare-fun esp0 () (_ BitVec 32))
(declare-fun OF0 () (_ BitVec 1))
(declare-fun SF0 () (_ BitVec 1))
(declare-fun ZF0 () (_ BitVec 1))
(declare-fun PF0 () (_ BitVec 1))
(declare-fun CF0 () (_ BitVec 1))
(declare-fun AF0 () (_ BitVec 1))
(declare-fun DF0 () (_ BitVec 1))
(declare-fun fs_base0 () (_ BitVec 32))
(define-fun temp320 () (_ BitVec 32) esp0)
(define-fun memory1 () (Array (_ BitVec 32) (_ BitVec 8)) (store (store (store (store memory0 (bvsub esp0 (_ bv4 32)) ((_ extract 7 0) eax0)) (bvsub esp0 (_ bv3 32)) ((_ extract 15 8) eax0)) (bvsub esp0 (_ bv2 32)) ((_ extract 23 16) eax0)) (bvsub esp0 (_ bv1 32)) ((_ extract 31 24) eax0)))
(define-fun esp1 () (_ BitVec 32) (bvsub esp0 (_ bv4 32)))
(define-fun memory2 () (Array (_ BitVec 32) (_ BitVec 8)) (store (store (store (store memory1 (bvsub esp1 (_ bv4 32)) ((_ extract 7 0) ecx0)) (bvsub esp1 (_ bv3 32)) ((_ extract 15 8) ecx0)) (bvsub esp1 (_ bv2 32)) ((_ extract 23 16) ecx0)) (bvsub esp1 (_ bv1 32)) ((_ extract 31 24) ecx0)))
(define-fun esp2 () (_ BitVec 32) (bvsub esp1 (_ bv4 32)))
(define-fun memory3 () (Array (_ BitVec 32) (_ BitVec 8)) (store (store (store (store memory2 (bvsub esp2 (_ bv4 32)) ((_ extract 7 0) edx0)) (bvsub esp2 (_ bv3 32)) ((_ extract 15 8) edx0)) (bvsub esp2 (_ bv2 32)) ((_ extract 23 16) edx0)) (bvsub esp2 (_ bv1 32)) ((_ extract 31 24) edx0)))
(define-fun esp3 () (_ BitVec 32) (bvsub esp2 (_ bv4 32)))
(define-fun memory4 () (Array (_ BitVec 32) (_ BitVec 8)) (store (store (store (store memory3 (bvsub esp3 (_ bv4 32)) ((_ extract 7 0) ebx0)) (bvsub esp3 (_ bv3 32)) ((_ extract 15 8) ebx0)) (bvsub esp3 (_ bv2 32)) ((_ extract 23 16) ebx0)) (bvsub esp3 (_ bv1 32)) ((_ extract 31 24) ebx0)))
(define-fun esp4 () (_ BitVec 32) (bvsub esp3 (_ bv4 32)))
(define-fun memory5 () (Array (_ BitVec 32) (_ BitVec 8)) (store (store (store (store memory4 (bvsub esp4 (_ bv4 32)) ((_ extract 7 0) temp320)) (bvsub esp4 (_ bv3 32)) ((_ extract 15 8) temp320)) (bvsub esp4 (_ bv2 32)) ((_ extract 23 16) temp320)) (bvsub esp4 (_ bv1 32)) ((_ extract 31 24) temp320)))
(define-fun esp5 () (_ BitVec 32) (bvsub esp4 (_ bv4 32)))
(define-fun memory6 () (Array (_ BitVec 32) (_ BitVec 8)) (store (store (store (store memory5 (bvsub esp5 (_ bv4 32)) ((_ extract 7 0) ebp0)) (bvsub esp5 (_ bv3 32)) ((_ extract 15 8) ebp0)) (bvsub esp5 (_ bv2 32)) ((_ extract 23 16) ebp0)) (bvsub esp5 (_ bv1 32)) ((_ extract 31 24) ebp0)))
(define-fun esp6 () (_ BitVec 32) (bvsub esp5 (_ bv4 32)))
(define-fun memory7 () (Array (_ BitVec 32) (_ BitVec 8)) (store (store (store (store memory6 (bvsub esp6 (_ bv4 32)) ((_ extract 7 0) esi0)) (bvsub esp6 (_ bv3 32)) ((_ extract 15 8) esi0)) (bvsub esp6 (_ bv2 32)) ((_ extract 23 16) esi0)) (bvsub esp6 (_ bv1 32)) ((_ extract 31 24) esi0)))
(define-fun esp7 () (_ BitVec 32) (bvsub esp6 (_ bv4 32)))
(define-fun memory8 () (Array (_ BitVec 32) (_ BitVec 8)) (store (store (store (store memory7 (bvsub esp7 (_ bv4 32)) ((_ extract 7 0) edi0)) (bvsub esp7 (_ bv3 32)) ((_ extract 15 8) edi0)) (bvsub esp7 (_ bv2 32)) ((_ extract 23 16) edi0)) (bvsub esp7 (_ bv1 32)) ((_ extract 31 24) edi0)))
(define-fun esp8 () (_ BitVec 32) (bvsub esp7 (_ bv4 32)))
(define-fun esp9 () (_ BitVec 32) (bvsub esp8 (_ bv4 32)))
(define-fun memory9 () (Array (_ BitVec 32) (_ BitVec 8)) (store (store (store (store memory8 esp9 (_ bv7 8)) (bvadd esp9 (_ bv1 32)) (_ bv80 8)) (bvadd esp9 (_ bv2 32)) (_ bv0 8)) (bvadd esp9 (_ bv3 32)) (_ bv1 8)))
(assert (= eax0 (_ bv0 32)))
(assert (= ebx0 (_ bv0 32)))
(assert (= ecx0 (_ bv0 32)))
(assert (= edx0 (_ bv0 32)))
(assert (= edi0 (_ bv0 32)))
(assert (= esi0 (_ bv0 32)))
(assert (= esp0 (_ bv458752 32)))
(assert (= ebp0 (_ bv458752 32)))
(check-sat)
(reset)




(set-option :produce-models true)
(set-logic QF_ABV)
(declare-fun memory0 () (Array (_ BitVec 32) (_ BitVec 8)))
(declare-fun eax0 () (_ BitVec 32))
(declare-fun ebx0 () (_ BitVec 32))
(declare-fun ecx0 () (_ BitVec 32))
(declare-fun edx0 () (_ BitVec 32))
(declare-fun esi0 () (_ BitVec 32))
(declare-fun edi0 () (_ BitVec 32))
(declare-fun ebp0 () (_ BitVec 32))
(declare-fun esp0 () (_ BitVec 32))
(declare-fun OF0 () (_ BitVec 1))
(declare-fun SF0 () (_ BitVec 1))
(declare-fun ZF0 () (_ BitVec 1))
(declare-fun PF0 () (_ BitVec 1))
(declare-fun CF0 () (_ BitVec 1))
(declare-fun AF0 () (_ BitVec 1))
(declare-fun DF0 () (_ BitVec 1))
(declare-fun fs_base0 () (_ BitVec 32))
(define-fun temp320 () (_ BitVec 32) esp0)
(define-fun memory1 () (Array (_ BitVec 32) (_ BitVec 8)) (store (store (store (store memory0 (bvsub esp0 (_ bv4 32)) ((_ extract 7 0) eax0)) (bvsub esp0 (_ bv3 32)) ((_ extract 15 8) eax0)) (bvsub esp0 (_ bv2 32)) ((_ extract 23 16) eax0)) (bvsub esp0 (_ bv1 32)) ((_ extract 31 24) eax0)))
(define-fun esp1 () (_ BitVec 32) (bvsub esp0 (_ bv4 32)))
(define-fun memory2 () (Array (_ BitVec 32) (_ BitVec 8)) (store (store (store (store memory1 (bvsub esp1 (_ bv4 32)) ((_ extract 7 0) ecx0)) (bvsub esp1 (_ bv3 32)) ((_ extract 15 8) ecx0)) (bvsub esp1 (_ bv2 32)) ((_ extract 23 16) ecx0)) (bvsub esp1 (_ bv1 32)) ((_ extract 31 24) ecx0)))
(define-fun esp2 () (_ BitVec 32) (bvsub esp1 (_ bv4 32)))
(define-fun memory3 () (Array (_ BitVec 32) (_ BitVec 8)) (store (store (store (store memory2 (bvsub esp2 (_ bv4 32)) ((_ extract 7 0) edx0)) (bvsub esp2 (_ bv3 32)) ((_ extract 15 8) edx0)) (bvsub esp2 (_ bv2 32)) ((_ extract 23 16) edx0)) (bvsub esp2 (_ bv1 32)) ((_ extract 31 24) edx0)))
(define-fun esp3 () (_ BitVec 32) (bvsub esp2 (_ bv4 32)))
(define-fun memory4 () (Array (_ BitVec 32) (_ BitVec 8)) (store (store (store (store memory3 (bvsub esp3 (_ bv4 32)) ((_ extract 7 0) ebx0)) (bvsub esp3 (_ bv3 32)) ((_ extract 15 8) ebx0)) (bvsub esp3 (_ bv2 32)) ((_ extract 23 16) ebx0)) (bvsub esp3 (_ bv1 32)) ((_ extract 31 24) ebx0)))
(define-fun esp4 () (_ BitVec 32) (bvsub esp3 (_ bv4 32)))
(define-fun memory5 () (Array (_ BitVec 32) (_ BitVec 8)) (store (store (store (store memory4 (bvsub esp4 (_ bv4 32)) ((_ extract 7 0) temp320)) (bvsub esp4 (_ bv3 32)) ((_ extract 15 8) temp320)) (bvsub esp4 (_ bv2 32)) ((_ extract 23 16) temp320)) (bvsub esp4 (_ bv1 32)) ((_ extract 31 24) temp320)))
(define-fun esp5 () (_ BitVec 32) (bvsub esp4 (_ bv4 32)))
(define-fun memory6 () (Array (_ BitVec 32) (_ BitVec 8)) (store (store (store (store memory5 (bvsub esp5 (_ bv4 32)) ((_ extract 7 0) ebp0)) (bvsub esp5 (_ bv3 32)) ((_ extract 15 8) ebp0)) (bvsub esp5 (_ bv2 32)) ((_ extract 23 16) ebp0)) (bvsub esp5 (_ bv1 32)) ((_ extract 31 24) ebp0)))
(define-fun esp6 () (_ BitVec 32) (bvsub esp5 (_ bv4 32)))
(define-fun memory7 () (Array (_ BitVec 32) (_ BitVec 8)) (store (store (store (store memory6 (bvsub esp6 (_ bv4 32)) ((_ extract 7 0) esi0)) (bvsub esp6 (_ bv3 32)) ((_ extract 15 8) esi0)) (bvsub esp6 (_ bv2 32)) ((_ extract 23 16) esi0)) (bvsub esp6 (_ bv1 32)) ((_ extract 31 24) esi0)))
(define-fun esp7 () (_ BitVec 32) (bvsub esp6 (_ bv4 32)))
(define-fun memory8 () (Array (_ BitVec 32) (_ BitVec 8)) (store (store (store (store memory7 (bvsub esp7 (_ bv4 32)) ((_ extract 7 0) edi0)) (bvsub esp7 (_ bv3 32)) ((_ extract 15 8) edi0)) (bvsub esp7 (_ bv2 32)) ((_ extract 23 16) edi0)) (bvsub esp7 (_ bv1 32)) ((_ extract 31 24) edi0)))
(define-fun esp8 () (_ BitVec 32) (bvsub esp7 (_ bv4 32)))
(define-fun esp9 () (_ BitVec 32) (bvsub esp8 (_ bv4 32)))
(define-fun memory9 () (Array (_ BitVec 32) (_ BitVec 8)) (store (store (store (store memory8 esp9 (_ bv7 8)) (bvadd esp9 (_ bv1 32)) (_ bv80 8)) (bvadd esp9 (_ bv2 32)) (_ bv0 8)) (bvadd esp9 (_ bv3 32)) (_ bv1 8)))
(assert (= eax0 (_ bv0 32)))
(assert (= ebx0 (_ bv0 32)))
(assert (= ecx0 (_ bv0 32)))
(assert (= edx0 (_ bv0 32)))
(assert (= edi0 (_ bv0 32)))
(assert (= esi0 (_ bv0 32)))
(assert (= esp0 (_ bv458752 32)))
(assert (= ebp0 (_ bv458752 32)))
(check-sat)
(reset)




(set-option :produce-models true)
(set-logic QF_ABV)
(declare-fun memory0 () (Array (_ BitVec 32) (_ BitVec 8)))
(declare-fun eax0 () (_ BitVec 32))
(declare-fun ebx0 () (_ BitVec 32))
(declare-fun ecx0 () (_ BitVec 32))
(declare-fun edx0 () (_ BitVec 32))
(declare-fun esi0 () (_ BitVec 32))
(declare-fun edi0 () (_ BitVec 32))
(declare-fun ebp0 () (_ BitVec 32))
(declare-fun esp0 () (_ BitVec 32))
(declare-fun OF0 () (_ BitVec 1))
(declare-fun SF0 () (_ BitVec 1))
(declare-fun ZF0 () (_ BitVec 1))
(declare-fun PF0 () (_ BitVec 1))
(declare-fun CF0 () (_ BitVec 1))
(declare-fun AF0 () (_ BitVec 1))
(declare-fun DF0 () (_ BitVec 1))
(declare-fun fs_base0 () (_ BitVec 32))
(define-fun temp320 () (_ BitVec 32) esp0)
(define-fun memory1 () (Array (_ BitVec 32) (_ BitVec 8)) (store (store (store (store memory0 (bvsub esp0 (_ bv4 32)) ((_ extract 7 0) eax0)) (bvsub esp0 (_ bv3 32)) ((_ extract 15 8) eax0)) (bvsub esp0 (_ bv2 32)) ((_ extract 23 16) eax0)) (bvsub esp0 (_ bv1 32)) ((_ extract 31 24) eax0)))
(define-fun esp1 () (_ BitVec 32) (bvsub esp0 (_ bv4 32)))
(define-fun memory2 () (Array (_ BitVec 32) (_ BitVec 8)) (store (store (store (store memory1 (bvsub esp1 (_ bv4 32)) ((_ extract 7 0) ecx0)) (bvsub esp1 (_ bv3 32)) ((_ extract 15 8) ecx0)) (bvsub esp1 (_ bv2 32)) ((_ extract 23 16) ecx0)) (bvsub esp1 (_ bv1 32)) ((_ extract 31 24) ecx0)))
(define-fun esp2 () (_ BitVec 32) (bvsub esp1 (_ bv4 32)))
(define-fun memory3 () (Array (_ BitVec 32) (_ BitVec 8)) (store (store (store (store memory2 (bvsub esp2 (_ bv4 32)) ((_ extract 7 0) edx0)) (bvsub esp2 (_ bv3 32)) ((_ extract 15 8) edx0)) (bvsub esp2 (_ bv2 32)) ((_ extract 23 16) edx0)) (bvsub esp2 (_ bv1 32)) ((_ extract 31 24) edx0)))
(define-fun esp3 () (_ BitVec 32) (bvsub esp2 (_ bv4 32)))
(define-fun memory4 () (Array (_ BitVec 32) (_ BitVec 8)) (store (store (store (store memory3 (bvsub esp3 (_ bv4 32)) ((_ extract 7 0) ebx0)) (bvsub esp3 (_ bv3 32)) ((_ extract 15 8) ebx0)) (bvsub esp3 (_ bv2 32)) ((_ extract 23 16) ebx0)) (bvsub esp3 (_ bv1 32)) ((_ extract 31 24) ebx0)))
(define-fun esp4 () (_ BitVec 32) (bvsub esp3 (_ bv4 32)))
(define-fun memory5 () (Array (_ BitVec 32) (_ BitVec 8)) (store (store (store (store memory4 (bvsub esp4 (_ bv4 32)) ((_ extract 7 0) temp320)) (bvsub esp4 (_ bv3 32)) ((_ extract 15 8) temp320)) (bvsub esp4 (_ bv2 32)) ((_ extract 23 16) temp320)) (bvsub esp4 (_ bv1 32)) ((_ extract 31 24) temp320)))
(define-fun esp5 () (_ BitVec 32) (bvsub esp4 (_ bv4 32)))
(define-fun memory6 () (Array (_ BitVec 32) (_ BitVec 8)) (store (store (store (store memory5 (bvsub esp5 (_ bv4 32)) ((_ extract 7 0) ebp0)) (bvsub esp5 (_ bv3 32)) ((_ extract 15 8) ebp0)) (bvsub esp5 (_ bv2 32)) ((_ extract 23 16) ebp0)) (bvsub esp5 (_ bv1 32)) ((_ extract 31 24) ebp0)))
(define-fun esp6 () (_ BitVec 32) (bvsub esp5 (_ bv4 32)))
(define-fun memory7 () (Array (_ BitVec 32) (_ BitVec 8)) (store (store (store (store memory6 (bvsub esp6 (_ bv4 32)) ((_ extract 7 0) esi0)) (bvsub esp6 (_ bv3 32)) ((_ extract 15 8) esi0)) (bvsub esp6 (_ bv2 32)) ((_ extract 23 16) esi0)) (bvsub esp6 (_ bv1 32)) ((_ extract 31 24) esi0)))
(define-fun esp7 () (_ BitVec 32) (bvsub esp6 (_ bv4 32)))
(define-fun memory8 () (Array (_ BitVec 32) (_ BitVec 8)) (store (store (store (store memory7 (bvsub esp7 (_ bv4 32)) ((_ extract 7 0) edi0)) (bvsub esp7 (_ bv3 32)) ((_ extract 15 8) edi0)) (bvsub esp7 (_ bv2 32)) ((_ extract 23 16) edi0)) (bvsub esp7 (_ bv1 32)) ((_ extract 31 24) edi0)))
(define-fun esp8 () (_ BitVec 32) (bvsub esp7 (_ bv4 32)))
(define-fun esp9 () (_ BitVec 32) (bvsub esp8 (_ bv4 32)))
(define-fun memory9 () (Array (_ BitVec 32) (_ BitVec 8)) (store (store (store (store memory8 esp9 (_ bv7 8)) (bvadd esp9 (_ bv1 32)) (_ bv80 8)) (bvadd esp9 (_ bv2 32)) (_ bv0 8)) (bvadd esp9 (_ bv3 32)) (_ bv1 8)))
(assert (= eax0 (_ bv0 32)))
(assert (= ebx0 (_ bv0 32)))
(assert (= ecx0 (_ bv0 32)))
(assert (= edx0 (_ bv0 32)))
(assert (= edi0 (_ bv0 32)))
(assert (= esi0 (_ bv0 32)))
(assert (= esp0 (_ bv458752 32)))
(assert (= ebp0 (_ bv458752 32)))
(check-sat)
(reset)




(set-option :produce-models true)
(set-logic QF_ABV)
(declare-fun memory0 () (Array (_ BitVec 32) (_ BitVec 8)))
(declare-fun eax0 () (_ BitVec 32))
(declare-fun ebx0 () (_ BitVec 32))
(declare-fun ecx0 () (_ BitVec 32))
(declare-fun edx0 () (_ BitVec 32))
(declare-fun esi0 () (_ BitVec 32))
(declare-fun edi0 () (_ BitVec 32))
(declare-fun ebp0 () (_ BitVec 32))
(declare-fun esp0 () (_ BitVec 32))
(declare-fun OF0 () (_ BitVec 1))
(declare-fun SF0 () (_ BitVec 1))
(declare-fun ZF0 () (_ BitVec 1))
(declare-fun PF0 () (_ BitVec 1))
(declare-fun CF0 () (_ BitVec 1))
(declare-fun AF0 () (_ BitVec 1))
(declare-fun DF0 () (_ BitVec 1))
(declare-fun fs_base0 () (_ BitVec 32))
(define-fun temp320 () (_ BitVec 32) esp0)
(define-fun memory1 () (Array (_ BitVec 32) (_ BitVec 8)) (store (store (store (store memory0 (bvsub esp0 (_ bv4 32)) ((_ extract 7 0) eax0)) (bvsub esp0 (_ bv3 32)) ((_ extract 15 8) eax0)) (bvsub esp0 (_ bv2 32)) ((_ extract 23 16) eax0)) (bvsub esp0 (_ bv1 32)) ((_ extract 31 24) eax0)))
(define-fun esp1 () (_ BitVec 32) (bvsub esp0 (_ bv4 32)))
(define-fun memory2 () (Array (_ BitVec 32) (_ BitVec 8)) (store (store (store (store memory1 (bvsub esp1 (_ bv4 32)) ((_ extract 7 0) ecx0)) (bvsub esp1 (_ bv3 32)) ((_ extract 15 8) ecx0)) (bvsub esp1 (_ bv2 32)) ((_ extract 23 16) ecx0)) (bvsub esp1 (_ bv1 32)) ((_ extract 31 24) ecx0)))
(define-fun esp2 () (_ BitVec 32) (bvsub esp1 (_ bv4 32)))
(define-fun memory3 () (Array (_ BitVec 32) (_ BitVec 8)) (store (store (store (store memory2 (bvsub esp2 (_ bv4 32)) ((_ extract 7 0) edx0)) (bvsub esp2 (_ bv3 32)) ((_ extract 15 8) edx0)) (bvsub esp2 (_ bv2 32)) ((_ extract 23 16) edx0)) (bvsub esp2 (_ bv1 32)) ((_ extract 31 24) edx0)))
(define-fun esp3 () (_ BitVec 32) (bvsub esp2 (_ bv4 32)))
(define-fun memory4 () (Array (_ BitVec 32) (_ BitVec 8)) (store (store (store (store memory3 (bvsub esp3 (_ bv4 32)) ((_ extract 7 0) ebx0)) (bvsub esp3 (_ bv3 32)) ((_ extract 15 8) ebx0)) (bvsub esp3 (_ bv2 32)) ((_ extract 23 16) ebx0)) (bvsub esp3 (_ bv1 32)) ((_ extract 31 24) ebx0)))
(define-fun esp4 () (_ BitVec 32) (bvsub esp3 (_ bv4 32)))
(define-fun memory5 () (Array (_ BitVec 32) (_ BitVec 8)) (store (store (store (store memory4 (bvsub esp4 (_ bv4 32)) ((_ extract 7 0) temp320)) (bvsub esp4 (_ bv3 32)) ((_ extract 15 8) temp320)) (bvsub esp4 (_ bv2 32)) ((_ extract 23 16) temp320)) (bvsub esp4 (_ bv1 32)) ((_ extract 31 24) temp320)))
(define-fun esp5 () (_ BitVec 32) (bvsub esp4 (_ bv4 32)))
(define-fun memory6 () (Array (_ BitVec 32) (_ BitVec 8)) (store (store (store (store memory5 (bvsub esp5 (_ bv4 32)) ((_ extract 7 0) ebp0)) (bvsub esp5 (_ bv3 32)) ((_ extract 15 8) ebp0)) (bvsub esp5 (_ bv2 32)) ((_ extract 23 16) ebp0)) (bvsub esp5 (_ bv1 32)) ((_ extract 31 24) ebp0)))
(define-fun esp6 () (_ BitVec 32) (bvsub esp5 (_ bv4 32)))
(define-fun memory7 () (Array (_ BitVec 32) (_ BitVec 8)) (store (store (store (store memory6 (bvsub esp6 (_ bv4 32)) ((_ extract 7 0) esi0)) (bvsub esp6 (_ bv3 32)) ((_ extract 15 8) esi0)) (bvsub esp6 (_ bv2 32)) ((_ extract 23 16) esi0)) (bvsub esp6 (_ bv1 32)) ((_ extract 31 24) esi0)))
(define-fun esp7 () (_ BitVec 32) (bvsub esp6 (_ bv4 32)))
(define-fun memory8 () (Array (_ BitVec 32) (_ BitVec 8)) (store (store (store (store memory7 (bvsub esp7 (_ bv4 32)) ((_ extract 7 0) edi0)) (bvsub esp7 (_ bv3 32)) ((_ extract 15 8) edi0)) (bvsub esp7 (_ bv2 32)) ((_ extract 23 16) edi0)) (bvsub esp7 (_ bv1 32)) ((_ extract 31 24) edi0)))
(define-fun esp8 () (_ BitVec 32) (bvsub esp7 (_ bv4 32)))
(define-fun esp9 () (_ BitVec 32) (bvsub esp8 (_ bv4 32)))
(define-fun memory9 () (Array (_ BitVec 32) (_ BitVec 8)) (store (store (store (store memory8 esp9 (_ bv7 8)) (bvadd esp9 (_ bv1 32)) (_ bv80 8)) (bvadd esp9 (_ bv2 32)) (_ bv0 8)) (bvadd esp9 (_ bv3 32)) (_ bv1 8)))
(assert (= eax0 (_ bv0 32)))
(assert (= ebx0 (_ bv0 32)))
(assert (= ecx0 (_ bv0 32)))
(assert (= edx0 (_ bv0 32)))
(assert (= edi0 (_ bv0 32)))
(assert (= esi0 (_ bv0 32)))
(assert (= esp0 (_ bv458752 32)))
(assert (= ebp0 (_ bv458752 32)))
(check-sat)
(reset)



(set-option :produce-models true)
(set-logic QF_ABV)
(declare-fun memory0 () (Array (_ BitVec 32) (_ BitVec 8)))
(declare-fun eax0 () (_ BitVec 32))
(declare-fun ebx0 () (_ BitVec 32))
(declare-fun ecx0 () (_ BitVec 32))
(declare-fun edx0 () (_ BitVec 32))
(declare-fun esi0 () (_ BitVec 32))
(declare-fun edi0 () (_ BitVec 32))
(declare-fun ebp0 () (_ BitVec 32))
(declare-fun esp0 () (_ BitVec 32))
(declare-fun OF0 () (_ BitVec 1))
(declare-fun SF0 () (_ BitVec 1))
(declare-fun ZF0 () (_ BitVec 1))
(declare-fun PF0 () (_ BitVec 1))
(declare-fun CF0 () (_ BitVec 1))
(declare-fun AF0 () (_ BitVec 1))
(declare-fun DF0 () (_ BitVec 1))
(declare-fun fs_base0 () (_ BitVec 32))
(define-fun temp320 () (_ BitVec 32) esp0)
(define-fun memory1 () (Array (_ BitVec 32) (_ BitVec 8)) (store (store (store (store memory0 (bvsub esp0 (_ bv4 32)) ((_ extract 7 0) eax0)) (bvsub esp0 (_ bv3 32)) ((_ extract 15 8) eax0)) (bvsub esp0 (_ bv2 32)) ((_ extract 23 16) eax0)) (bvsub esp0 (_ bv1 32)) ((_ extract 31 24) eax0)))
(define-fun esp1 () (_ BitVec 32) (bvsub esp0 (_ bv4 32)))
(define-fun memory2 () (Array (_ BitVec 32) (_ BitVec 8)) (store (store (store (store memory1 (bvsub esp1 (_ bv4 32)) ((_ extract 7 0) ecx0)) (bvsub esp1 (_ bv3 32)) ((_ extract 15 8) ecx0)) (bvsub esp1 (_ bv2 32)) ((_ extract 23 16) ecx0)) (bvsub esp1 (_ bv1 32)) ((_ extract 31 24) ecx0)))
(define-fun esp2 () (_ BitVec 32) (bvsub esp1 (_ bv4 32)))
(define-fun memory3 () (Array (_ BitVec 32) (_ BitVec 8)) (store (store (store (store memory2 (bvsub esp2 (_ bv4 32)) ((_ extract 7 0) edx0)) (bvsub esp2 (_ bv3 32)) ((_ extract 15 8) edx0)) (bvsub esp2 (_ bv2 32)) ((_ extract 23 16) edx0)) (bvsub esp2 (_ bv1 32)) ((_ extract 31 24) edx0)))
(define-fun esp3 () (_ BitVec 32) (bvsub esp2 (_ bv4 32)))
(define-fun memory4 () (Array (_ BitVec 32) (_ BitVec 8)) (store (store (store (store memory3 (bvsub esp3 (_ bv4 32)) ((_ extract 7 0) ebx0)) (bvsub esp3 (_ bv3 32)) ((_ extract 15 8) ebx0)) (bvsub esp3 (_ bv2 32)) ((_ extract 23 16) ebx0)) (bvsub esp3 (_ bv1 32)) ((_ extract 31 24) ebx0)))
(define-fun esp4 () (_ BitVec 32) (bvsub esp3 (_ bv4 32)))
(define-fun memory5 () (Array (_ BitVec 32) (_ BitVec 8)) (store (store (store (store memory4 (bvsub esp4 (_ bv4 32)) ((_ extract 7 0) temp320)) (bvsub esp4 (_ bv3 32)) ((_ extract 15 8) temp320)) (bvsub esp4 (_ bv2 32)) ((_ extract 23 16) temp320)) (bvsub esp4 (_ bv1 32)) ((_ extract 31 24) temp320)))
(define-fun esp5 () (_ BitVec 32) (bvsub esp4 (_ bv4 32)))
(define-fun memory6 () (Array (_ BitVec 32) (_ BitVec 8)) (store (store (store (store memory5 (bvsub esp5 (_ bv4 32)) ((_ extract 7 0) ebp0)) (bvsub esp5 (_ bv3 32)) ((_ extract 15 8) ebp0)) (bvsub esp5 (_ bv2 32)) ((_ extract 23 16) ebp0)) (bvsub esp5 (_ bv1 32)) ((_ extract 31 24) ebp0)))
(define-fun esp6 () (_ BitVec 32) (bvsub esp5 (_ bv4 32)))
(define-fun memory7 () (Array (_ BitVec 32) (_ BitVec 8)) (store (store (store (store memory6 (bvsub esp6 (_ bv4 32)) ((_ extract 7 0) esi0)) (bvsub esp6 (_ bv3 32)) ((_ extract 15 8) esi0)) (bvsub esp6 (_ bv2 32)) ((_ extract 23 16) esi0)) (bvsub esp6 (_ bv1 32)) ((_ extract 31 24) esi0)))
(define-fun esp7 () (_ BitVec 32) (bvsub esp6 (_ bv4 32)))
(define-fun memory8 () (Array (_ BitVec 32) (_ BitVec 8)) (store (store (store (store memory7 (bvsub esp7 (_ bv4 32)) ((_ extract 7 0) edi0)) (bvsub esp7 (_ bv3 32)) ((_ extract 15 8) edi0)) (bvsub esp7 (_ bv2 32)) ((_ extract 23 16) edi0)) (bvsub esp7 (_ bv1 32)) ((_ extract 31 24) edi0)))
(define-fun esp8 () (_ BitVec 32) (bvsub esp7 (_ bv4 32)))
(define-fun esp9 () (_ BitVec 32) (bvsub esp8 (_ bv4 32)))
(define-fun memory9 () (Array (_ BitVec 32) (_ BitVec 8)) (store (store (store (store memory8 esp9 (_ bv7 8)) (bvadd esp9 (_ bv1 32)) (_ bv80 8)) (bvadd esp9 (_ bv2 32)) (_ bv0 8)) (bvadd esp9 (_ bv3 32)) (_ bv1 8)))
(assert (= eax0 (_ bv0 32)))
(assert (= ebx0 (_ bv0 32)))
(assert (= ecx0 (_ bv0 32)))
(assert (= edx0 (_ bv0 32)))
(assert (= edi0 (_ bv0 32)))
(assert (= esi0 (_ bv0 32)))
(assert (= esp0 (_ bv458752 32)))
(assert (= ebp0 (_ bv458752 32)))
(check-sat)
(reset)



(set-option :produce-models true)
(set-logic QF_ABV)
(declare-fun memory0 () (Array (_ BitVec 32) (_ BitVec 8)))
(declare-fun eax0 () (_ BitVec 32))
(declare-fun ebx0 () (_ BitVec 32))
(declare-fun ecx0 () (_ BitVec 32))
(declare-fun edx0 () (_ BitVec 32))
(declare-fun esi0 () (_ BitVec 32))
(declare-fun edi0 () (_ BitVec 32))
(declare-fun ebp0 () (_ BitVec 32))
(declare-fun esp0 () (_ BitVec 32))
(declare-fun OF0 () (_ BitVec 1))
(declare-fun SF0 () (_ BitVec 1))
(declare-fun ZF0 () (_ BitVec 1))
(declare-fun PF0 () (_ BitVec 1))
(declare-fun CF0 () (_ BitVec 1))
(declare-fun AF0 () (_ BitVec 1))
(declare-fun DF0 () (_ BitVec 1))
(declare-fun fs_base0 () (_ BitVec 32))
(define-fun temp320 () (_ BitVec 32) esp0)
(define-fun memory1 () (Array (_ BitVec 32) (_ BitVec 8)) (store (store (store (store memory0 (bvsub esp0 (_ bv4 32)) ((_ extract 7 0) eax0)) (bvsub esp0 (_ bv3 32)) ((_ extract 15 8) eax0)) (bvsub esp0 (_ bv2 32)) ((_ extract 23 16) eax0)) (bvsub esp0 (_ bv1 32)) ((_ extract 31 24) eax0)))
(define-fun esp1 () (_ BitVec 32) (bvsub esp0 (_ bv4 32)))
(define-fun memory2 () (Array (_ BitVec 32) (_ BitVec 8)) (store (store (store (store memory1 (bvsub esp1 (_ bv4 32)) ((_ extract 7 0) ecx0)) (bvsub esp1 (_ bv3 32)) ((_ extract 15 8) ecx0)) (bvsub esp1 (_ bv2 32)) ((_ extract 23 16) ecx0)) (bvsub esp1 (_ bv1 32)) ((_ extract 31 24) ecx0)))
(define-fun esp2 () (_ BitVec 32) (bvsub esp1 (_ bv4 32)))
(define-fun memory3 () (Array (_ BitVec 32) (_ BitVec 8)) (store (store (store (store memory2 (bvsub esp2 (_ bv4 32)) ((_ extract 7 0) edx0)) (bvsub esp2 (_ bv3 32)) ((_ extract 15 8) edx0)) (bvsub esp2 (_ bv2 32)) ((_ extract 23 16) edx0)) (bvsub esp2 (_ bv1 32)) ((_ extract 31 24) edx0)))
(define-fun esp3 () (_ BitVec 32) (bvsub esp2 (_ bv4 32)))
(define-fun memory4 () (Array (_ BitVec 32) (_ BitVec 8)) (store (store (store (store memory3 (bvsub esp3 (_ bv4 32)) ((_ extract 7 0) ebx0)) (bvsub esp3 (_ bv3 32)) ((_ extract 15 8) ebx0)) (bvsub esp3 (_ bv2 32)) ((_ extract 23 16) ebx0)) (bvsub esp3 (_ bv1 32)) ((_ extract 31 24) ebx0)))
(define-fun esp4 () (_ BitVec 32) (bvsub esp3 (_ bv4 32)))
(define-fun memory5 () (Array (_ BitVec 32) (_ BitVec 8)) (store (store (store (store memory4 (bvsub esp4 (_ bv4 32)) ((_ extract 7 0) temp320)) (bvsub esp4 (_ bv3 32)) ((_ extract 15 8) temp320)) (bvsub esp4 (_ bv2 32)) ((_ extract 23 16) temp320)) (bvsub esp4 (_ bv1 32)) ((_ extract 31 24) temp320)))
(define-fun esp5 () (_ BitVec 32) (bvsub esp4 (_ bv4 32)))
(define-fun memory6 () (Array (_ BitVec 32) (_ BitVec 8)) (store (store (store (store memory5 (bvsub esp5 (_ bv4 32)) ((_ extract 7 0) ebp0)) (bvsub esp5 (_ bv3 32)) ((_ extract 15 8) ebp0)) (bvsub esp5 (_ bv2 32)) ((_ extract 23 16) ebp0)) (bvsub esp5 (_ bv1 32)) ((_ extract 31 24) ebp0)))
(define-fun esp6 () (_ BitVec 32) (bvsub esp5 (_ bv4 32)))
(define-fun memory7 () (Array (_ BitVec 32) (_ BitVec 8)) (store (store (store (store memory6 (bvsub esp6 (_ bv4 32)) ((_ extract 7 0) esi0)) (bvsub esp6 (_ bv3 32)) ((_ extract 15 8) esi0)) (bvsub esp6 (_ bv2 32)) ((_ extract 23 16) esi0)) (bvsub esp6 (_ bv1 32)) ((_ extract 31 24) esi0)))
(define-fun esp7 () (_ BitVec 32) (bvsub esp6 (_ bv4 32)))
(define-fun memory8 () (Array (_ BitVec 32) (_ BitVec 8)) (store (store (store (store memory7 (bvsub esp7 (_ bv4 32)) ((_ extract 7 0) edi0)) (bvsub esp7 (_ bv3 32)) ((_ extract 15 8) edi0)) (bvsub esp7 (_ bv2 32)) ((_ extract 23 16) edi0)) (bvsub esp7 (_ bv1 32)) ((_ extract 31 24) edi0)))
(define-fun esp8 () (_ BitVec 32) (bvsub esp7 (_ bv4 32)))
(define-fun esp9 () (_ BitVec 32) (bvsub esp8 (_ bv4 32)))
(define-fun memory9 () (Array (_ BitVec 32) (_ BitVec 8)) (store (store (store (store memory8 esp9 (_ bv7 8)) (bvadd esp9 (_ bv1 32)) (_ bv80 8)) (bvadd esp9 (_ bv2 32)) (_ bv0 8)) (bvadd esp9 (_ bv3 32)) (_ bv1 8)))
(assert (= eax0 (_ bv0 32)))
(assert (= ebx0 (_ bv0 32)))
(assert (= ecx0 (_ bv0 32)))
(assert (= edx0 (_ bv0 32)))
(assert (= edi0 (_ bv0 32)))
(assert (= esi0 (_ bv0 32)))
(assert (= esp0 (_ bv458752 32)))
(assert (= ebp0 (_ bv458752 32)))
(check-sat)
(reset)



(set-option :produce-models true)
(set-logic QF_ABV)
(declare-fun memory0 () (Array (_ BitVec 32) (_ BitVec 8)))
(declare-fun eax0 () (_ BitVec 32))
(declare-fun ebx0 () (_ BitVec 32))
(declare-fun ecx0 () (_ BitVec 32))
(declare-fun edx0 () (_ BitVec 32))
(declare-fun esi0 () (_ BitVec 32))
(declare-fun edi0 () (_ BitVec 32))
(declare-fun ebp0 () (_ BitVec 32))
(declare-fun esp0 () (_ BitVec 32))
(declare-fun OF0 () (_ BitVec 1))
(declare-fun SF0 () (_ BitVec 1))
(declare-fun ZF0 () (_ BitVec 1))
(declare-fun PF0 () (_ BitVec 1))
(declare-fun CF0 () (_ BitVec 1))
(declare-fun AF0 () (_ BitVec 1))
(declare-fun DF0 () (_ BitVec 1))
(declare-fun fs_base0 () (_ BitVec 32))
(define-fun temp320 () (_ BitVec 32) esp0)
(define-fun memory1 () (Array (_ BitVec 32) (_ BitVec 8)) (store (store (store (store memory0 (bvsub esp0 (_ bv4 32)) ((_ extract 7 0) eax0)) (bvsub esp0 (_ bv3 32)) ((_ extract 15 8) eax0)) (bvsub esp0 (_ bv2 32)) ((_ extract 23 16) eax0)) (bvsub esp0 (_ bv1 32)) ((_ extract 31 24) eax0)))
(define-fun esp1 () (_ BitVec 32) (bvsub esp0 (_ bv4 32)))
(define-fun memory2 () (Array (_ BitVec 32) (_ BitVec 8)) (store (store (store (store memory1 (bvsub esp1 (_ bv4 32)) ((_ extract 7 0) ecx0)) (bvsub esp1 (_ bv3 32)) ((_ extract 15 8) ecx0)) (bvsub esp1 (_ bv2 32)) ((_ extract 23 16) ecx0)) (bvsub esp1 (_ bv1 32)) ((_ extract 31 24) ecx0)))
(define-fun esp2 () (_ BitVec 32) (bvsub esp1 (_ bv4 32)))
(define-fun memory3 () (Array (_ BitVec 32) (_ BitVec 8)) (store (store (store (store memory2 (bvsub esp2 (_ bv4 32)) ((_ extract 7 0) edx0)) (bvsub esp2 (_ bv3 32)) ((_ extract 15 8) edx0)) (bvsub esp2 (_ bv2 32)) ((_ extract 23 16) edx0)) (bvsub esp2 (_ bv1 32)) ((_ extract 31 24) edx0)))
(define-fun esp3 () (_ BitVec 32) (bvsub esp2 (_ bv4 32)))
(define-fun memory4 () (Array (_ BitVec 32) (_ BitVec 8)) (store (store (store (store memory3 (bvsub esp3 (_ bv4 32)) ((_ extract 7 0) ebx0)) (bvsub esp3 (_ bv3 32)) ((_ extract 15 8) ebx0)) (bvsub esp3 (_ bv2 32)) ((_ extract 23 16) ebx0)) (bvsub esp3 (_ bv1 32)) ((_ extract 31 24) ebx0)))
(define-fun esp4 () (_ BitVec 32) (bvsub esp3 (_ bv4 32)))
(define-fun memory5 () (Array (_ BitVec 32) (_ BitVec 8)) (store (store (store (store memory4 (bvsub esp4 (_ bv4 32)) ((_ extract 7 0) temp320)) (bvsub esp4 (_ bv3 32)) ((_ extract 15 8) temp320)) (bvsub esp4 (_ bv2 32)) ((_ extract 23 16) temp320)) (bvsub esp4 (_ bv1 32)) ((_ extract 31 24) temp320)))
(define-fun esp5 () (_ BitVec 32) (bvsub esp4 (_ bv4 32)))
(define-fun memory6 () (Array (_ BitVec 32) (_ BitVec 8)) (store (store (store (store memory5 (bvsub esp5 (_ bv4 32)) ((_ extract 7 0) ebp0)) (bvsub esp5 (_ bv3 32)) ((_ extract 15 8) ebp0)) (bvsub esp5 (_ bv2 32)) ((_ extract 23 16) ebp0)) (bvsub esp5 (_ bv1 32)) ((_ extract 31 24) ebp0)))
(define-fun esp6 () (_ BitVec 32) (bvsub esp5 (_ bv4 32)))
(define-fun memory7 () (Array (_ BitVec 32) (_ BitVec 8)) (store (store (store (store memory6 (bvsub esp6 (_ bv4 32)) ((_ extract 7 0) esi0)) (bvsub esp6 (_ bv3 32)) ((_ extract 15 8) esi0)) (bvsub esp6 (_ bv2 32)) ((_ extract 23 16) esi0)) (bvsub esp6 (_ bv1 32)) ((_ extract 31 24) esi0)))
(define-fun esp7 () (_ BitVec 32) (bvsub esp6 (_ bv4 32)))
(define-fun memory8 () (Array (_ BitVec 32) (_ BitVec 8)) (store (store (store (store memory7 (bvsub esp7 (_ bv4 32)) ((_ extract 7 0) edi0)) (bvsub esp7 (_ bv3 32)) ((_ extract 15 8) edi0)) (bvsub esp7 (_ bv2 32)) ((_ extract 23 16) edi0)) (bvsub esp7 (_ bv1 32)) ((_ extract 31 24) edi0)))
(define-fun esp8 () (_ BitVec 32) (bvsub esp7 (_ bv4 32)))
(define-fun esp9 () (_ BitVec 32) (bvsub esp8 (_ bv4 32)))
(define-fun memory9 () (Array (_ BitVec 32) (_ BitVec 8)) (store (store (store (store memory8 esp9 (_ bv7 8)) (bvadd esp9 (_ bv1 32)) (_ bv80 8)) (bvadd esp9 (_ bv2 32)) (_ bv0 8)) (bvadd esp9 (_ bv3 32)) (_ bv1 8)))
(assert (= eax0 (_ bv0 32)))
(assert (= ebx0 (_ bv0 32)))
(assert (= ecx0 (_ bv0 32)))
(assert (= edx0 (_ bv0 32)))
(assert (= edi0 (_ bv0 32)))
(assert (= esi0 (_ bv0 32)))
(assert (= esp0 (_ bv458752 32)))
(assert (= ebp0 (_ bv458752 32)))
(check-sat)
(reset)



(set-option :produce-models true)
(set-logic QF_ABV)
(declare-fun memory0 () (Array (_ BitVec 32) (_ BitVec 8)))
(declare-fun eax0 () (_ BitVec 32))
(declare-fun ebx0 () (_ BitVec 32))
(declare-fun ecx0 () (_ BitVec 32))
(declare-fun edx0 () (_ BitVec 32))
(declare-fun esi0 () (_ BitVec 32))
(declare-fun edi0 () (_ BitVec 32))
(declare-fun ebp0 () (_ BitVec 32))
(declare-fun esp0 () (_ BitVec 32))
(declare-fun OF0 () (_ BitVec 1))
(declare-fun SF0 () (_ BitVec 1))
(declare-fun ZF0 () (_ BitVec 1))
(declare-fun PF0 () (_ BitVec 1))
(declare-fun CF0 () (_ BitVec 1))
(declare-fun AF0 () (_ BitVec 1))
(declare-fun DF0 () (_ BitVec 1))
(declare-fun fs_base0 () (_ BitVec 32))
(define-fun temp320 () (_ BitVec 32) esp0)
(define-fun memory1 () (Array (_ BitVec 32) (_ BitVec 8)) (store (store (store (store memory0 (bvsub esp0 (_ bv4 32)) ((_ extract 7 0) eax0)) (bvsub esp0 (_ bv3 32)) ((_ extract 15 8) eax0)) (bvsub esp0 (_ bv2 32)) ((_ extract 23 16) eax0)) (bvsub esp0 (_ bv1 32)) ((_ extract 31 24) eax0)))
(define-fun esp1 () (_ BitVec 32) (bvsub esp0 (_ bv4 32)))
(define-fun memory2 () (Array (_ BitVec 32) (_ BitVec 8)) (store (store (store (store memory1 (bvsub esp1 (_ bv4 32)) ((_ extract 7 0) ecx0)) (bvsub esp1 (_ bv3 32)) ((_ extract 15 8) ecx0)) (bvsub esp1 (_ bv2 32)) ((_ extract 23 16) ecx0)) (bvsub esp1 (_ bv1 32)) ((_ extract 31 24) ecx0)))
(define-fun esp2 () (_ BitVec 32) (bvsub esp1 (_ bv4 32)))
(define-fun memory3 () (Array (_ BitVec 32) (_ BitVec 8)) (store (store (store (store memory2 (bvsub esp2 (_ bv4 32)) ((_ extract 7 0) edx0)) (bvsub esp2 (_ bv3 32)) ((_ extract 15 8) edx0)) (bvsub esp2 (_ bv2 32)) ((_ extract 23 16) edx0)) (bvsub esp2 (_ bv1 32)) ((_ extract 31 24) edx0)))
(define-fun esp3 () (_ BitVec 32) (bvsub esp2 (_ bv4 32)))
(define-fun memory4 () (Array (_ BitVec 32) (_ BitVec 8)) (store (store (store (store memory3 (bvsub esp3 (_ bv4 32)) ((_ extract 7 0) ebx0)) (bvsub esp3 (_ bv3 32)) ((_ extract 15 8) ebx0)) (bvsub esp3 (_ bv2 32)) ((_ extract 23 16) ebx0)) (bvsub esp3 (_ bv1 32)) ((_ extract 31 24) ebx0)))
(define-fun esp4 () (_ BitVec 32) (bvsub esp3 (_ bv4 32)))
(define-fun memory5 () (Array (_ BitVec 32) (_ BitVec 8)) (store (store (store (store memory4 (bvsub esp4 (_ bv4 32)) ((_ extract 7 0) temp320)) (bvsub esp4 (_ bv3 32)) ((_ extract 15 8) temp320)) (bvsub esp4 (_ bv2 32)) ((_ extract 23 16) temp320)) (bvsub esp4 (_ bv1 32)) ((_ extract 31 24) temp320)))
(define-fun esp5 () (_ BitVec 32) (bvsub esp4 (_ bv4 32)))
(define-fun memory6 () (Array (_ BitVec 32) (_ BitVec 8)) (store (store (store (store memory5 (bvsub esp5 (_ bv4 32)) ((_ extract 7 0) ebp0)) (bvsub esp5 (_ bv3 32)) ((_ extract 15 8) ebp0)) (bvsub esp5 (_ bv2 32)) ((_ extract 23 16) ebp0)) (bvsub esp5 (_ bv1 32)) ((_ extract 31 24) ebp0)))
(define-fun esp6 () (_ BitVec 32) (bvsub esp5 (_ bv4 32)))
(define-fun memory7 () (Array (_ BitVec 32) (_ BitVec 8)) (store (store (store (store memory6 (bvsub esp6 (_ bv4 32)) ((_ extract 7 0) esi0)) (bvsub esp6 (_ bv3 32)) ((_ extract 15 8) esi0)) (bvsub esp6 (_ bv2 32)) ((_ extract 23 16) esi0)) (bvsub esp6 (_ bv1 32)) ((_ extract 31 24) esi0)))
(define-fun esp7 () (_ BitVec 32) (bvsub esp6 (_ bv4 32)))
(define-fun memory8 () (Array (_ BitVec 32) (_ BitVec 8)) (store (store (store (store memory7 (bvsub esp7 (_ bv4 32)) ((_ extract 7 0) edi0)) (bvsub esp7 (_ bv3 32)) ((_ extract 15 8) edi0)) (bvsub esp7 (_ bv2 32)) ((_ extract 23 16) edi0)) (bvsub esp7 (_ bv1 32)) ((_ extract 31 24) edi0)))
(define-fun esp8 () (_ BitVec 32) (bvsub esp7 (_ bv4 32)))
(define-fun esp9 () (_ BitVec 32) (bvsub esp8 (_ bv4 32)))
(define-fun memory9 () (Array (_ BitVec 32) (_ BitVec 8)) (store (store (store (store memory8 esp9 (_ bv7 8)) (bvadd esp9 (_ bv1 32)) (_ bv80 8)) (bvadd esp9 (_ bv2 32)) (_ bv0 8)) (bvadd esp9 (_ bv3 32)) (_ bv1 8)))
(assert (= eax0 (_ bv0 32)))
(assert (= ebx0 (_ bv0 32)))
(assert (= ecx0 (_ bv0 32)))
(assert (= edx0 (_ bv0 32)))
(assert (= edi0 (_ bv0 32)))
(assert (= esi0 (_ bv0 32)))
(assert (= esp0 (_ bv458752 32)))
(assert (= ebp0 (_ bv458752 32)))
(check-sat)
(reset)



(set-option :produce-models true)
(set-logic QF_ABV)
(declare-fun memory0 () (Array (_ BitVec 32) (_ BitVec 8)))
(declare-fun eax0 () (_ BitVec 32))
(declare-fun ebx0 () (_ BitVec 32))
(declare-fun ecx0 () (_ BitVec 32))
(declare-fun edx0 () (_ BitVec 32))
(declare-fun esi0 () (_ BitVec 32))
(declare-fun edi0 () (_ BitVec 32))
(declare-fun ebp0 () (_ BitVec 32))
(declare-fun esp0 () (_ BitVec 32))
(declare-fun OF0 () (_ BitVec 1))
(declare-fun SF0 () (_ BitVec 1))
(declare-fun ZF0 () (_ BitVec 1))
(declare-fun PF0 () (_ BitVec 1))
(declare-fun CF0 () (_ BitVec 1))
(declare-fun AF0 () (_ BitVec 1))
(declare-fun DF0 () (_ BitVec 1))
(declare-fun fs_base0 () (_ BitVec 32))
(define-fun temp320 () (_ BitVec 32) esp0)
(define-fun memory1 () (Array (_ BitVec 32) (_ BitVec 8)) (store (store (store (store memory0 (bvsub esp0 (_ bv4 32)) ((_ extract 7 0) eax0)) (bvsub esp0 (_ bv3 32)) ((_ extract 15 8) eax0)) (bvsub esp0 (_ bv2 32)) ((_ extract 23 16) eax0)) (bvsub esp0 (_ bv1 32)) ((_ extract 31 24) eax0)))
(define-fun esp1 () (_ BitVec 32) (bvsub esp0 (_ bv4 32)))
(define-fun memory2 () (Array (_ BitVec 32) (_ BitVec 8)) (store (store (store (store memory1 (bvsub esp1 (_ bv4 32)) ((_ extract 7 0) ecx0)) (bvsub esp1 (_ bv3 32)) ((_ extract 15 8) ecx0)) (bvsub esp1 (_ bv2 32)) ((_ extract 23 16) ecx0)) (bvsub esp1 (_ bv1 32)) ((_ extract 31 24) ecx0)))
(define-fun esp2 () (_ BitVec 32) (bvsub esp1 (_ bv4 32)))
(define-fun memory3 () (Array (_ BitVec 32) (_ BitVec 8)) (store (store (store (store memory2 (bvsub esp2 (_ bv4 32)) ((_ extract 7 0) edx0)) (bvsub esp2 (_ bv3 32)) ((_ extract 15 8) edx0)) (bvsub esp2 (_ bv2 32)) ((_ extract 23 16) edx0)) (bvsub esp2 (_ bv1 32)) ((_ extract 31 24) edx0)))
(define-fun esp3 () (_ BitVec 32) (bvsub esp2 (_ bv4 32)))
(define-fun memory4 () (Array (_ BitVec 32) (_ BitVec 8)) (store (store (store (store memory3 (bvsub esp3 (_ bv4 32)) ((_ extract 7 0) ebx0)) (bvsub esp3 (_ bv3 32)) ((_ extract 15 8) ebx0)) (bvsub esp3 (_ bv2 32)) ((_ extract 23 16) ebx0)) (bvsub esp3 (_ bv1 32)) ((_ extract 31 24) ebx0)))
(define-fun esp4 () (_ BitVec 32) (bvsub esp3 (_ bv4 32)))
(define-fun memory5 () (Array (_ BitVec 32) (_ BitVec 8)) (store (store (store (store memory4 (bvsub esp4 (_ bv4 32)) ((_ extract 7 0) temp320)) (bvsub esp4 (_ bv3 32)) ((_ extract 15 8) temp320)) (bvsub esp4 (_ bv2 32)) ((_ extract 23 16) temp320)) (bvsub esp4 (_ bv1 32)) ((_ extract 31 24) temp320)))
(define-fun esp5 () (_ BitVec 32) (bvsub esp4 (_ bv4 32)))
(define-fun memory6 () (Array (_ BitVec 32) (_ BitVec 8)) (store (store (store (store memory5 (bvsub esp5 (_ bv4 32)) ((_ extract 7 0) ebp0)) (bvsub esp5 (_ bv3 32)) ((_ extract 15 8) ebp0)) (bvsub esp5 (_ bv2 32)) ((_ extract 23 16) ebp0)) (bvsub esp5 (_ bv1 32)) ((_ extract 31 24) ebp0)))
(define-fun esp6 () (_ BitVec 32) (bvsub esp5 (_ bv4 32)))
(define-fun memory7 () (Array (_ BitVec 32) (_ BitVec 8)) (store (store (store (store memory6 (bvsub esp6 (_ bv4 32)) ((_ extract 7 0) esi0)) (bvsub esp6 (_ bv3 32)) ((_ extract 15 8) esi0)) (bvsub esp6 (_ bv2 32)) ((_ extract 23 16) esi0)) (bvsub esp6 (_ bv1 32)) ((_ extract 31 24) esi0)))
(define-fun esp7 () (_ BitVec 32) (bvsub esp6 (_ bv4 32)))
(define-fun memory8 () (Array (_ BitVec 32) (_ BitVec 8)) (store (store (store (store memory7 (bvsub esp7 (_ bv4 32)) ((_ extract 7 0) edi0)) (bvsub esp7 (_ bv3 32)) ((_ extract 15 8) edi0)) (bvsub esp7 (_ bv2 32)) ((_ extract 23 16) edi0)) (bvsub esp7 (_ bv1 32)) ((_ extract 31 24) edi0)))
(define-fun esp8 () (_ BitVec 32) (bvsub esp7 (_ bv4 32)))
(define-fun esp9 () (_ BitVec 32) (bvsub esp8 (_ bv4 32)))
(define-fun memory9 () (Array (_ BitVec 32) (_ BitVec 8)) (store (store (store (store memory8 esp9 (_ bv7 8)) (bvadd esp9 (_ bv1 32)) (_ bv80 8)) (bvadd esp9 (_ bv2 32)) (_ bv0 8)) (bvadd esp9 (_ bv3 32)) (_ bv1 8)))
(assert (= eax0 (_ bv0 32)))
(assert (= ebx0 (_ bv0 32)))
(assert (= ecx0 (_ bv0 32)))
(assert (= edx0 (_ bv0 32)))
(assert (= edi0 (_ bv0 32)))
(assert (= esi0 (_ bv0 32)))
(assert (= esp0 (_ bv458752 32)))
(assert (= ebp0 (_ bv458752 32)))
(check-sat)
(reset)



(set-option :produce-models true)
(set-logic QF_ABV)
(declare-fun memory0 () (Array (_ BitVec 32) (_ BitVec 8)))
(declare-fun eax0 () (_ BitVec 32))
(declare-fun ebx0 () (_ BitVec 32))
(declare-fun ecx0 () (_ BitVec 32))
(declare-fun edx0 () (_ BitVec 32))
(declare-fun esi0 () (_ BitVec 32))
(declare-fun edi0 () (_ BitVec 32))
(declare-fun ebp0 () (_ BitVec 32))
(declare-fun esp0 () (_ BitVec 32))
(declare-fun OF0 () (_ BitVec 1))
(declare-fun SF0 () (_ BitVec 1))
(declare-fun ZF0 () (_ BitVec 1))
(declare-fun PF0 () (_ BitVec 1))
(declare-fun CF0 () (_ BitVec 1))
(declare-fun AF0 () (_ BitVec 1))
(declare-fun DF0 () (_ BitVec 1))
(declare-fun fs_base0 () (_ BitVec 32))
(define-fun temp320 () (_ BitVec 32) esp0)
(define-fun memory1 () (Array (_ BitVec 32) (_ BitVec 8)) (store (store (store (store memory0 (bvsub esp0 (_ bv4 32)) ((_ extract 7 0) eax0)) (bvsub esp0 (_ bv3 32)) ((_ extract 15 8) eax0)) (bvsub esp0 (_ bv2 32)) ((_ extract 23 16) eax0)) (bvsub esp0 (_ bv1 32)) ((_ extract 31 24) eax0)))
(define-fun esp1 () (_ BitVec 32) (bvsub esp0 (_ bv4 32)))
(define-fun memory2 () (Array (_ BitVec 32) (_ BitVec 8)) (store (store (store (store memory1 (bvsub esp1 (_ bv4 32)) ((_ extract 7 0) ecx0)) (bvsub esp1 (_ bv3 32)) ((_ extract 15 8) ecx0)) (bvsub esp1 (_ bv2 32)) ((_ extract 23 16) ecx0)) (bvsub esp1 (_ bv1 32)) ((_ extract 31 24) ecx0)))
(define-fun esp2 () (_ BitVec 32) (bvsub esp1 (_ bv4 32)))
(define-fun memory3 () (Array (_ BitVec 32) (_ BitVec 8)) (store (store (store (store memory2 (bvsub esp2 (_ bv4 32)) ((_ extract 7 0) edx0)) (bvsub esp2 (_ bv3 32)) ((_ extract 15 8) edx0)) (bvsub esp2 (_ bv2 32)) ((_ extract 23 16) edx0)) (bvsub esp2 (_ bv1 32)) ((_ extract 31 24) edx0)))
(define-fun esp3 () (_ BitVec 32) (bvsub esp2 (_ bv4 32)))
(define-fun memory4 () (Array (_ BitVec 32) (_ BitVec 8)) (store (store (store (store memory3 (bvsub esp3 (_ bv4 32)) ((_ extract 7 0) ebx0)) (bvsub esp3 (_ bv3 32)) ((_ extract 15 8) ebx0)) (bvsub esp3 (_ bv2 32)) ((_ extract 23 16) ebx0)) (bvsub esp3 (_ bv1 32)) ((_ extract 31 24) ebx0)))
(define-fun esp4 () (_ BitVec 32) (bvsub esp3 (_ bv4 32)))
(define-fun memory5 () (Array (_ BitVec 32) (_ BitVec 8)) (store (store (store (store memory4 (bvsub esp4 (_ bv4 32)) ((_ extract 7 0) temp320)) (bvsub esp4 (_ bv3 32)) ((_ extract 15 8) temp320)) (bvsub esp4 (_ bv2 32)) ((_ extract 23 16) temp320)) (bvsub esp4 (_ bv1 32)) ((_ extract 31 24) temp320)))
(define-fun esp5 () (_ BitVec 32) (bvsub esp4 (_ bv4 32)))
(define-fun memory6 () (Array (_ BitVec 32) (_ BitVec 8)) (store (store (store (store memory5 (bvsub esp5 (_ bv4 32)) ((_ extract 7 0) ebp0)) (bvsub esp5 (_ bv3 32)) ((_ extract 15 8) ebp0)) (bvsub esp5 (_ bv2 32)) ((_ extract 23 16) ebp0)) (bvsub esp5 (_ bv1 32)) ((_ extract 31 24) ebp0)))
(define-fun esp6 () (_ BitVec 32) (bvsub esp5 (_ bv4 32)))
(define-fun memory7 () (Array (_ BitVec 32) (_ BitVec 8)) (store (store (store (store memory6 (bvsub esp6 (_ bv4 32)) ((_ extract 7 0) esi0)) (bvsub esp6 (_ bv3 32)) ((_ extract 15 8) esi0)) (bvsub esp6 (_ bv2 32)) ((_ extract 23 16) esi0)) (bvsub esp6 (_ bv1 32)) ((_ extract 31 24) esi0)))
(define-fun esp7 () (_ BitVec 32) (bvsub esp6 (_ bv4 32)))
(define-fun memory8 () (Array (_ BitVec 32) (_ BitVec 8)) (store (store (store (store memory7 (bvsub esp7 (_ bv4 32)) ((_ extract 7 0) edi0)) (bvsub esp7 (_ bv3 32)) ((_ extract 15 8) edi0)) (bvsub esp7 (_ bv2 32)) ((_ extract 23 16) edi0)) (bvsub esp7 (_ bv1 32)) ((_ extract 31 24) edi0)))
(define-fun esp8 () (_ BitVec 32) (bvsub esp7 (_ bv4 32)))
(define-fun esp9 () (_ BitVec 32) (bvsub esp8 (_ bv4 32)))
(define-fun memory9 () (Array (_ BitVec 32) (_ BitVec 8)) (store (store (store (store memory8 esp9 (_ bv7 8)) (bvadd esp9 (_ bv1 32)) (_ bv80 8)) (bvadd esp9 (_ bv2 32)) (_ bv0 8)) (bvadd esp9 (_ bv3 32)) (_ bv1 8)))
(assert (= eax0 (_ bv0 32)))
(assert (= ebx0 (_ bv0 32)))
(assert (= ecx0 (_ bv0 32)))
(assert (= edx0 (_ bv0 32)))
(assert (= edi0 (_ bv0 32)))
(assert (= esi0 (_ bv0 32)))
(assert (= esp0 (_ bv458752 32)))
(assert (= ebp0 (_ bv458752 32)))
(check-sat)
(reset)



(set-option :produce-models true)
(set-logic QF_ABV)
(declare-fun memory0 () (Array (_ BitVec 32) (_ BitVec 8)))
(declare-fun eax0 () (_ BitVec 32))
(declare-fun ebx0 () (_ BitVec 32))
(declare-fun ecx0 () (_ BitVec 32))
(declare-fun edx0 () (_ BitVec 32))
(declare-fun esi0 () (_ BitVec 32))
(declare-fun edi0 () (_ BitVec 32))
(declare-fun ebp0 () (_ BitVec 32))
(declare-fun esp0 () (_ BitVec 32))
(declare-fun OF0 () (_ BitVec 1))
(declare-fun SF0 () (_ BitVec 1))
(declare-fun ZF0 () (_ BitVec 1))
(declare-fun PF0 () (_ BitVec 1))
(declare-fun CF0 () (_ BitVec 1))
(declare-fun AF0 () (_ BitVec 1))
(declare-fun DF0 () (_ BitVec 1))
(declare-fun fs_base0 () (_ BitVec 32))
(define-fun temp320 () (_ BitVec 32) esp0)
(define-fun memory1 () (Array (_ BitVec 32) (_ BitVec 8)) (store (store (store (store memory0 (bvsub esp0 (_ bv4 32)) ((_ extract 7 0) eax0)) (bvsub esp0 (_ bv3 32)) ((_ extract 15 8) eax0)) (bvsub esp0 (_ bv2 32)) ((_ extract 23 16) eax0)) (bvsub esp0 (_ bv1 32)) ((_ extract 31 24) eax0)))
(define-fun esp1 () (_ BitVec 32) (bvsub esp0 (_ bv4 32)))
(define-fun memory2 () (Array (_ BitVec 32) (_ BitVec 8)) (store (store (store (store memory1 (bvsub esp1 (_ bv4 32)) ((_ extract 7 0) ecx0)) (bvsub esp1 (_ bv3 32)) ((_ extract 15 8) ecx0)) (bvsub esp1 (_ bv2 32)) ((_ extract 23 16) ecx0)) (bvsub esp1 (_ bv1 32)) ((_ extract 31 24) ecx0)))
(define-fun esp2 () (_ BitVec 32) (bvsub esp1 (_ bv4 32)))
(define-fun memory3 () (Array (_ BitVec 32) (_ BitVec 8)) (store (store (store (store memory2 (bvsub esp2 (_ bv4 32)) ((_ extract 7 0) edx0)) (bvsub esp2 (_ bv3 32)) ((_ extract 15 8) edx0)) (bvsub esp2 (_ bv2 32)) ((_ extract 23 16) edx0)) (bvsub esp2 (_ bv1 32)) ((_ extract 31 24) edx0)))
(define-fun esp3 () (_ BitVec 32) (bvsub esp2 (_ bv4 32)))
(define-fun memory4 () (Array (_ BitVec 32) (_ BitVec 8)) (store (store (store (store memory3 (bvsub esp3 (_ bv4 32)) ((_ extract 7 0) ebx0)) (bvsub esp3 (_ bv3 32)) ((_ extract 15 8) ebx0)) (bvsub esp3 (_ bv2 32)) ((_ extract 23 16) ebx0)) (bvsub esp3 (_ bv1 32)) ((_ extract 31 24) ebx0)))
(define-fun esp4 () (_ BitVec 32) (bvsub esp3 (_ bv4 32)))
(define-fun memory5 () (Array (_ BitVec 32) (_ BitVec 8)) (store (store (store (store memory4 (bvsub esp4 (_ bv4 32)) ((_ extract 7 0) temp320)) (bvsub esp4 (_ bv3 32)) ((_ extract 15 8) temp320)) (bvsub esp4 (_ bv2 32)) ((_ extract 23 16) temp320)) (bvsub esp4 (_ bv1 32)) ((_ extract 31 24) temp320)))
(define-fun esp5 () (_ BitVec 32) (bvsub esp4 (_ bv4 32)))
(define-fun memory6 () (Array (_ BitVec 32) (_ BitVec 8)) (store (store (store (store memory5 (bvsub esp5 (_ bv4 32)) ((_ extract 7 0) ebp0)) (bvsub esp5 (_ bv3 32)) ((_ extract 15 8) ebp0)) (bvsub esp5 (_ bv2 32)) ((_ extract 23 16) ebp0)) (bvsub esp5 (_ bv1 32)) ((_ extract 31 24) ebp0)))
(define-fun esp6 () (_ BitVec 32) (bvsub esp5 (_ bv4 32)))
(define-fun memory7 () (Array (_ BitVec 32) (_ BitVec 8)) (store (store (store (store memory6 (bvsub esp6 (_ bv4 32)) ((_ extract 7 0) esi0)) (bvsub esp6 (_ bv3 32)) ((_ extract 15 8) esi0)) (bvsub esp6 (_ bv2 32)) ((_ extract 23 16) esi0)) (bvsub esp6 (_ bv1 32)) ((_ extract 31 24) esi0)))
(define-fun esp7 () (_ BitVec 32) (bvsub esp6 (_ bv4 32)))
(define-fun memory8 () (Array (_ BitVec 32) (_ BitVec 8)) (store (store (store (store memory7 (bvsub esp7 (_ bv4 32)) ((_ extract 7 0) edi0)) (bvsub esp7 (_ bv3 32)) ((_ extract 15 8) edi0)) (bvsub esp7 (_ bv2 32)) ((_ extract 23 16) edi0)) (bvsub esp7 (_ bv1 32)) ((_ extract 31 24) edi0)))
(define-fun esp8 () (_ BitVec 32) (bvsub esp7 (_ bv4 32)))
(define-fun esp9 () (_ BitVec 32) (bvsub esp8 (_ bv4 32)))
(define-fun memory9 () (Array (_ BitVec 32) (_ BitVec 8)) (store (store (store (store memory8 esp9 (_ bv7 8)) (bvadd esp9 (_ bv1 32)) (_ bv80 8)) (bvadd esp9 (_ bv2 32)) (_ bv0 8)) (bvadd esp9 (_ bv3 32)) (_ bv1 8)))
(assert (= eax0 (_ bv0 32)))
(assert (= ebx0 (_ bv0 32)))
(assert (= ecx0 (_ bv0 32)))
(assert (= edx0 (_ bv0 32)))
(assert (= edi0 (_ bv0 32)))
(assert (= esi0 (_ bv0 32)))
(assert (= esp0 (_ bv458752 32)))
(assert (= ebp0 (_ bv458752 32)))
(check-sat)
(reset)



(set-option :produce-models true)
(set-logic QF_ABV)
(declare-fun memory0 () (Array (_ BitVec 32) (_ BitVec 8)))
(declare-fun eax0 () (_ BitVec 32))
(declare-fun ebx0 () (_ BitVec 32))
(declare-fun ecx0 () (_ BitVec 32))
(declare-fun edx0 () (_ BitVec 32))
(declare-fun esi0 () (_ BitVec 32))
(declare-fun edi0 () (_ BitVec 32))
(declare-fun ebp0 () (_ BitVec 32))
(declare-fun esp0 () (_ BitVec 32))
(declare-fun OF0 () (_ BitVec 1))
(declare-fun SF0 () (_ BitVec 1))
(declare-fun ZF0 () (_ BitVec 1))
(declare-fun PF0 () (_ BitVec 1))
(declare-fun CF0 () (_ BitVec 1))
(declare-fun AF0 () (_ BitVec 1))
(declare-fun DF0 () (_ BitVec 1))
(declare-fun fs_base0 () (_ BitVec 32))
(define-fun temp320 () (_ BitVec 32) esp0)
(define-fun memory1 () (Array (_ BitVec 32) (_ BitVec 8)) (store (store (store (store memory0 (bvsub esp0 (_ bv4 32)) ((_ extract 7 0) eax0)) (bvsub esp0 (_ bv3 32)) ((_ extract 15 8) eax0)) (bvsub esp0 (_ bv2 32)) ((_ extract 23 16) eax0)) (bvsub esp0 (_ bv1 32)) ((_ extract 31 24) eax0)))
(define-fun esp1 () (_ BitVec 32) (bvsub esp0 (_ bv4 32)))
(define-fun memory2 () (Array (_ BitVec 32) (_ BitVec 8)) (store (store (store (store memory1 (bvsub esp1 (_ bv4 32)) ((_ extract 7 0) ecx0)) (bvsub esp1 (_ bv3 32)) ((_ extract 15 8) ecx0)) (bvsub esp1 (_ bv2 32)) ((_ extract 23 16) ecx0)) (bvsub esp1 (_ bv1 32)) ((_ extract 31 24) ecx0)))
(define-fun esp2 () (_ BitVec 32) (bvsub esp1 (_ bv4 32)))
(define-fun memory3 () (Array (_ BitVec 32) (_ BitVec 8)) (store (store (store (store memory2 (bvsub esp2 (_ bv4 32)) ((_ extract 7 0) edx0)) (bvsub esp2 (_ bv3 32)) ((_ extract 15 8) edx0)) (bvsub esp2 (_ bv2 32)) ((_ extract 23 16) edx0)) (bvsub esp2 (_ bv1 32)) ((_ extract 31 24) edx0)))
(define-fun esp3 () (_ BitVec 32) (bvsub esp2 (_ bv4 32)))
(define-fun memory4 () (Array (_ BitVec 32) (_ BitVec 8)) (store (store (store (store memory3 (bvsub esp3 (_ bv4 32)) ((_ extract 7 0) ebx0)) (bvsub esp3 (_ bv3 32)) ((_ extract 15 8) ebx0)) (bvsub esp3 (_ bv2 32)) ((_ extract 23 16) ebx0)) (bvsub esp3 (_ bv1 32)) ((_ extract 31 24) ebx0)))
(define-fun esp4 () (_ BitVec 32) (bvsub esp3 (_ bv4 32)))
(define-fun memory5 () (Array (_ BitVec 32) (_ BitVec 8)) (store (store (store (store memory4 (bvsub esp4 (_ bv4 32)) ((_ extract 7 0) temp320)) (bvsub esp4 (_ bv3 32)) ((_ extract 15 8) temp320)) (bvsub esp4 (_ bv2 32)) ((_ extract 23 16) temp320)) (bvsub esp4 (_ bv1 32)) ((_ extract 31 24) temp320)))
(define-fun esp5 () (_ BitVec 32) (bvsub esp4 (_ bv4 32)))
(define-fun memory6 () (Array (_ BitVec 32) (_ BitVec 8)) (store (store (store (store memory5 (bvsub esp5 (_ bv4 32)) ((_ extract 7 0) ebp0)) (bvsub esp5 (_ bv3 32)) ((_ extract 15 8) ebp0)) (bvsub esp5 (_ bv2 32)) ((_ extract 23 16) ebp0)) (bvsub esp5 (_ bv1 32)) ((_ extract 31 24) ebp0)))
(define-fun esp6 () (_ BitVec 32) (bvsub esp5 (_ bv4 32)))
(define-fun memory7 () (Array (_ BitVec 32) (_ BitVec 8)) (store (store (store (store memory6 (bvsub esp6 (_ bv4 32)) ((_ extract 7 0) esi0)) (bvsub esp6 (_ bv3 32)) ((_ extract 15 8) esi0)) (bvsub esp6 (_ bv2 32)) ((_ extract 23 16) esi0)) (bvsub esp6 (_ bv1 32)) ((_ extract 31 24) esi0)))
(define-fun esp7 () (_ BitVec 32) (bvsub esp6 (_ bv4 32)))
(define-fun memory8 () (Array (_ BitVec 32) (_ BitVec 8)) (store (store (store (store memory7 (bvsub esp7 (_ bv4 32)) ((_ extract 7 0) edi0)) (bvsub esp7 (_ bv3 32)) ((_ extract 15 8) edi0)) (bvsub esp7 (_ bv2 32)) ((_ extract 23 16) edi0)) (bvsub esp7 (_ bv1 32)) ((_ extract 31 24) edi0)))
(define-fun esp8 () (_ BitVec 32) (bvsub esp7 (_ bv4 32)))
(define-fun esp9 () (_ BitVec 32) (bvsub esp8 (_ bv4 32)))
(define-fun memory9 () (Array (_ BitVec 32) (_ BitVec 8)) (store (store (store (store memory8 esp9 (_ bv7 8)) (bvadd esp9 (_ bv1 32)) (_ bv80 8)) (bvadd esp9 (_ bv2 32)) (_ bv0 8)) (bvadd esp9 (_ bv3 32)) (_ bv1 8)))
(assert (= eax0 (_ bv0 32)))
(assert (= ebx0 (_ bv0 32)))
(assert (= ecx0 (_ bv0 32)))
(assert (= edx0 (_ bv0 32)))
(assert (= edi0 (_ bv0 32)))
(assert (= esi0 (_ bv0 32)))
(assert (= esp0 (_ bv458752 32)))
(assert (= ebp0 (_ bv458752 32)))
(check-sat)
(reset)



(set-option :produce-models true)
(set-logic QF_ABV)
(declare-fun memory0 () (Array (_ BitVec 32) (_ BitVec 8)))
(declare-fun eax0 () (_ BitVec 32))
(declare-fun ebx0 () (_ BitVec 32))
(declare-fun ecx0 () (_ BitVec 32))
(declare-fun edx0 () (_ BitVec 32))
(declare-fun esi0 () (_ BitVec 32))
(declare-fun edi0 () (_ BitVec 32))
(declare-fun ebp0 () (_ BitVec 32))
(declare-fun esp0 () (_ BitVec 32))
(declare-fun OF0 () (_ BitVec 1))
(declare-fun SF0 () (_ BitVec 1))
(declare-fun ZF0 () (_ BitVec 1))
(declare-fun PF0 () (_ BitVec 1))
(declare-fun CF0 () (_ BitVec 1))
(declare-fun AF0 () (_ BitVec 1))
(declare-fun DF0 () (_ BitVec 1))
(declare-fun fs_base0 () (_ BitVec 32))
(define-fun temp320 () (_ BitVec 32) esp0)
(define-fun memory1 () (Array (_ BitVec 32) (_ BitVec 8)) (store (store (store (store memory0 (bvsub esp0 (_ bv4 32)) ((_ extract 7 0) eax0)) (bvsub esp0 (_ bv3 32)) ((_ extract 15 8) eax0)) (bvsub esp0 (_ bv2 32)) ((_ extract 23 16) eax0)) (bvsub esp0 (_ bv1 32)) ((_ extract 31 24) eax0)))
(define-fun esp1 () (_ BitVec 32) (bvsub esp0 (_ bv4 32)))
(define-fun memory2 () (Array (_ BitVec 32) (_ BitVec 8)) (store (store (store (store memory1 (bvsub esp1 (_ bv4 32)) ((_ extract 7 0) ecx0)) (bvsub esp1 (_ bv3 32)) ((_ extract 15 8) ecx0)) (bvsub esp1 (_ bv2 32)) ((_ extract 23 16) ecx0)) (bvsub esp1 (_ bv1 32)) ((_ extract 31 24) ecx0)))
(define-fun esp2 () (_ BitVec 32) (bvsub esp1 (_ bv4 32)))
(define-fun memory3 () (Array (_ BitVec 32) (_ BitVec 8)) (store (store (store (store memory2 (bvsub esp2 (_ bv4 32)) ((_ extract 7 0) edx0)) (bvsub esp2 (_ bv3 32)) ((_ extract 15 8) edx0)) (bvsub esp2 (_ bv2 32)) ((_ extract 23 16) edx0)) (bvsub esp2 (_ bv1 32)) ((_ extract 31 24) edx0)))
(define-fun esp3 () (_ BitVec 32) (bvsub esp2 (_ bv4 32)))
(define-fun memory4 () (Array (_ BitVec 32) (_ BitVec 8)) (store (store (store (store memory3 (bvsub esp3 (_ bv4 32)) ((_ extract 7 0) ebx0)) (bvsub esp3 (_ bv3 32)) ((_ extract 15 8) ebx0)) (bvsub esp3 (_ bv2 32)) ((_ extract 23 16) ebx0)) (bvsub esp3 (_ bv1 32)) ((_ extract 31 24) ebx0)))
(define-fun esp4 () (_ BitVec 32) (bvsub esp3 (_ bv4 32)))
(define-fun memory5 () (Array (_ BitVec 32) (_ BitVec 8)) (store (store (store (store memory4 (bvsub esp4 (_ bv4 32)) ((_ extract 7 0) temp320)) (bvsub esp4 (_ bv3 32)) ((_ extract 15 8) temp320)) (bvsub esp4 (_ bv2 32)) ((_ extract 23 16) temp320)) (bvsub esp4 (_ bv1 32)) ((_ extract 31 24) temp320)))
(define-fun esp5 () (_ BitVec 32) (bvsub esp4 (_ bv4 32)))
(define-fun memory6 () (Array (_ BitVec 32) (_ BitVec 8)) (store (store (store (store memory5 (bvsub esp5 (_ bv4 32)) ((_ extract 7 0) ebp0)) (bvsub esp5 (_ bv3 32)) ((_ extract 15 8) ebp0)) (bvsub esp5 (_ bv2 32)) ((_ extract 23 16) ebp0)) (bvsub esp5 (_ bv1 32)) ((_ extract 31 24) ebp0)))
(define-fun esp6 () (_ BitVec 32) (bvsub esp5 (_ bv4 32)))
(define-fun memory7 () (Array (_ BitVec 32) (_ BitVec 8)) (store (store (store (store memory6 (bvsub esp6 (_ bv4 32)) ((_ extract 7 0) esi0)) (bvsub esp6 (_ bv3 32)) ((_ extract 15 8) esi0)) (bvsub esp6 (_ bv2 32)) ((_ extract 23 16) esi0)) (bvsub esp6 (_ bv1 32)) ((_ extract 31 24) esi0)))
(define-fun esp7 () (_ BitVec 32) (bvsub esp6 (_ bv4 32)))
(define-fun memory8 () (Array (_ BitVec 32) (_ BitVec 8)) (store (store (store (store memory7 (bvsub esp7 (_ bv4 32)) ((_ extract 7 0) edi0)) (bvsub esp7 (_ bv3 32)) ((_ extract 15 8) edi0)) (bvsub esp7 (_ bv2 32)) ((_ extract 23 16) edi0)) (bvsub esp7 (_ bv1 32)) ((_ extract 31 24) edi0)))
(define-fun esp8 () (_ BitVec 32) (bvsub esp7 (_ bv4 32)))
(define-fun esp9 () (_ BitVec 32) (bvsub esp8 (_ bv4 32)))
(define-fun memory9 () (Array (_ BitVec 32) (_ BitVec 8)) (store (store (store (store memory8 esp9 (_ bv7 8)) (bvadd esp9 (_ bv1 32)) (_ bv80 8)) (bvadd esp9 (_ bv2 32)) (_ bv0 8)) (bvadd esp9 (_ bv3 32)) (_ bv1 8)))
(assert (= eax0 (_ bv0 32)))
(assert (= ebx0 (_ bv0 32)))
(assert (= ecx0 (_ bv0 32)))
(assert (= edx0 (_ bv0 32)))
(assert (= edi0 (_ bv0 32)))
(assert (= esi0 (_ bv0 32)))
(assert (= esp0 (_ bv458752 32)))
(assert (= ebp0 (_ bv458752 32)))
(check-sat)
(reset)



(set-option :produce-models true)
(set-logic QF_ABV)
(declare-fun memory0 () (Array (_ BitVec 32) (_ BitVec 8)))
(declare-fun eax0 () (_ BitVec 32))
(declare-fun ebx0 () (_ BitVec 32))
(declare-fun ecx0 () (_ BitVec 32))
(declare-fun edx0 () (_ BitVec 32))
(declare-fun esi0 () (_ BitVec 32))
(declare-fun edi0 () (_ BitVec 32))
(declare-fun ebp0 () (_ BitVec 32))
(declare-fun esp0 () (_ BitVec 32))
(declare-fun OF0 () (_ BitVec 1))
(declare-fun SF0 () (_ BitVec 1))
(declare-fun ZF0 () (_ BitVec 1))
(declare-fun PF0 () (_ BitVec 1))
(declare-fun CF0 () (_ BitVec 1))
(declare-fun AF0 () (_ BitVec 1))
(declare-fun DF0 () (_ BitVec 1))
(declare-fun fs_base0 () (_ BitVec 32))
(define-fun temp320 () (_ BitVec 32) esp0)
(define-fun memory1 () (Array (_ BitVec 32) (_ BitVec 8)) (store (store (store (store memory0 (bvsub esp0 (_ bv4 32)) ((_ extract 7 0) eax0)) (bvsub esp0 (_ bv3 32)) ((_ extract 15 8) eax0)) (bvsub esp0 (_ bv2 32)) ((_ extract 23 16) eax0)) (bvsub esp0 (_ bv1 32)) ((_ extract 31 24) eax0)))
(define-fun esp1 () (_ BitVec 32) (bvsub esp0 (_ bv4 32)))
(define-fun memory2 () (Array (_ BitVec 32) (_ BitVec 8)) (store (store (store (store memory1 (bvsub esp1 (_ bv4 32)) ((_ extract 7 0) ecx0)) (bvsub esp1 (_ bv3 32)) ((_ extract 15 8) ecx0)) (bvsub esp1 (_ bv2 32)) ((_ extract 23 16) ecx0)) (bvsub esp1 (_ bv1 32)) ((_ extract 31 24) ecx0)))
(define-fun esp2 () (_ BitVec 32) (bvsub esp1 (_ bv4 32)))
(define-fun memory3 () (Array (_ BitVec 32) (_ BitVec 8)) (store (store (store (store memory2 (bvsub esp2 (_ bv4 32)) ((_ extract 7 0) edx0)) (bvsub esp2 (_ bv3 32)) ((_ extract 15 8) edx0)) (bvsub esp2 (_ bv2 32)) ((_ extract 23 16) edx0)) (bvsub esp2 (_ bv1 32)) ((_ extract 31 24) edx0)))
(define-fun esp3 () (_ BitVec 32) (bvsub esp2 (_ bv4 32)))
(define-fun memory4 () (Array (_ BitVec 32) (_ BitVec 8)) (store (store (store (store memory3 (bvsub esp3 (_ bv4 32)) ((_ extract 7 0) ebx0)) (bvsub esp3 (_ bv3 32)) ((_ extract 15 8) ebx0)) (bvsub esp3 (_ bv2 32)) ((_ extract 23 16) ebx0)) (bvsub esp3 (_ bv1 32)) ((_ extract 31 24) ebx0)))
(define-fun esp4 () (_ BitVec 32) (bvsub esp3 (_ bv4 32)))
(define-fun memory5 () (Array (_ BitVec 32) (_ BitVec 8)) (store (store (store (store memory4 (bvsub esp4 (_ bv4 32)) ((_ extract 7 0) temp320)) (bvsub esp4 (_ bv3 32)) ((_ extract 15 8) temp320)) (bvsub esp4 (_ bv2 32)) ((_ extract 23 16) temp320)) (bvsub esp4 (_ bv1 32)) ((_ extract 31 24) temp320)))
(define-fun esp5 () (_ BitVec 32) (bvsub esp4 (_ bv4 32)))
(define-fun memory6 () (Array (_ BitVec 32) (_ BitVec 8)) (store (store (store (store memory5 (bvsub esp5 (_ bv4 32)) ((_ extract 7 0) ebp0)) (bvsub esp5 (_ bv3 32)) ((_ extract 15 8) ebp0)) (bvsub esp5 (_ bv2 32)) ((_ extract 23 16) ebp0)) (bvsub esp5 (_ bv1 32)) ((_ extract 31 24) ebp0)))
(define-fun esp6 () (_ BitVec 32) (bvsub esp5 (_ bv4 32)))
(define-fun memory7 () (Array (_ BitVec 32) (_ BitVec 8)) (store (store (store (store memory6 (bvsub esp6 (_ bv4 32)) ((_ extract 7 0) esi0)) (bvsub esp6 (_ bv3 32)) ((_ extract 15 8) esi0)) (bvsub esp6 (_ bv2 32)) ((_ extract 23 16) esi0)) (bvsub esp6 (_ bv1 32)) ((_ extract 31 24) esi0)))
(define-fun esp7 () (_ BitVec 32) (bvsub esp6 (_ bv4 32)))
(define-fun memory8 () (Array (_ BitVec 32) (_ BitVec 8)) (store (store (store (store memory7 (bvsub esp7 (_ bv4 32)) ((_ extract 7 0) edi0)) (bvsub esp7 (_ bv3 32)) ((_ extract 15 8) edi0)) (bvsub esp7 (_ bv2 32)) ((_ extract 23 16) edi0)) (bvsub esp7 (_ bv1 32)) ((_ extract 31 24) edi0)))
(define-fun esp8 () (_ BitVec 32) (bvsub esp7 (_ bv4 32)))
(define-fun esp9 () (_ BitVec 32) (bvsub esp8 (_ bv4 32)))
(define-fun memory9 () (Array (_ BitVec 32) (_ BitVec 8)) (store (store (store (store memory8 esp9 (_ bv7 8)) (bvadd esp9 (_ bv1 32)) (_ bv80 8)) (bvadd esp9 (_ bv2 32)) (_ bv0 8)) (bvadd esp9 (_ bv3 32)) (_ bv1 8)))
(assert (= eax0 (_ bv0 32)))
(assert (= ebx0 (_ bv0 32)))
(assert (= ecx0 (_ bv0 32)))
(assert (= edx0 (_ bv0 32)))
(assert (= edi0 (_ bv0 32)))
(assert (= esi0 (_ bv0 32)))
(assert (= esp0 (_ bv458752 32)))
(assert (= ebp0 (_ bv458752 32)))
(check-sat)
(reset)



(set-option :produce-models true)
(set-logic QF_ABV)
(declare-fun memory0 () (Array (_ BitVec 32) (_ BitVec 8)))
(declare-fun eax0 () (_ BitVec 32))
(declare-fun ebx0 () (_ BitVec 32))
(declare-fun ecx0 () (_ BitVec 32))
(declare-fun edx0 () (_ BitVec 32))
(declare-fun esi0 () (_ BitVec 32))
(declare-fun edi0 () (_ BitVec 32))
(declare-fun ebp0 () (_ BitVec 32))
(declare-fun esp0 () (_ BitVec 32))
(declare-fun OF0 () (_ BitVec 1))
(declare-fun SF0 () (_ BitVec 1))
(declare-fun ZF0 () (_ BitVec 1))
(declare-fun PF0 () (_ BitVec 1))
(declare-fun CF0 () (_ BitVec 1))
(declare-fun AF0 () (_ BitVec 1))
(declare-fun DF0 () (_ BitVec 1))
(declare-fun fs_base0 () (_ BitVec 32))
(define-fun temp320 () (_ BitVec 32) esp0)
(define-fun memory1 () (Array (_ BitVec 32) (_ BitVec 8)) (store (store (store (store memory0 (bvsub esp0 (_ bv4 32)) ((_ extract 7 0) eax0)) (bvsub esp0 (_ bv3 32)) ((_ extract 15 8) eax0)) (bvsub esp0 (_ bv2 32)) ((_ extract 23 16) eax0)) (bvsub esp0 (_ bv1 32)) ((_ extract 31 24) eax0)))
(define-fun esp1 () (_ BitVec 32) (bvsub esp0 (_ bv4 32)))
(define-fun memory2 () (Array (_ BitVec 32) (_ BitVec 8)) (store (store (store (store memory1 (bvsub esp1 (_ bv4 32)) ((_ extract 7 0) ecx0)) (bvsub esp1 (_ bv3 32)) ((_ extract 15 8) ecx0)) (bvsub esp1 (_ bv2 32)) ((_ extract 23 16) ecx0)) (bvsub esp1 (_ bv1 32)) ((_ extract 31 24) ecx0)))
(define-fun esp2 () (_ BitVec 32) (bvsub esp1 (_ bv4 32)))
(define-fun memory3 () (Array (_ BitVec 32) (_ BitVec 8)) (store (store (store (store memory2 (bvsub esp2 (_ bv4 32)) ((_ extract 7 0) edx0)) (bvsub esp2 (_ bv3 32)) ((_ extract 15 8) edx0)) (bvsub esp2 (_ bv2 32)) ((_ extract 23 16) edx0)) (bvsub esp2 (_ bv1 32)) ((_ extract 31 24) edx0)))
(define-fun esp3 () (_ BitVec 32) (bvsub esp2 (_ bv4 32)))
(define-fun memory4 () (Array (_ BitVec 32) (_ BitVec 8)) (store (store (store (store memory3 (bvsub esp3 (_ bv4 32)) ((_ extract 7 0) ebx0)) (bvsub esp3 (_ bv3 32)) ((_ extract 15 8) ebx0)) (bvsub esp3 (_ bv2 32)) ((_ extract 23 16) ebx0)) (bvsub esp3 (_ bv1 32)) ((_ extract 31 24) ebx0)))
(define-fun esp4 () (_ BitVec 32) (bvsub esp3 (_ bv4 32)))
(define-fun memory5 () (Array (_ BitVec 32) (_ BitVec 8)) (store (store (store (store memory4 (bvsub esp4 (_ bv4 32)) ((_ extract 7 0) temp320)) (bvsub esp4 (_ bv3 32)) ((_ extract 15 8) temp320)) (bvsub esp4 (_ bv2 32)) ((_ extract 23 16) temp320)) (bvsub esp4 (_ bv1 32)) ((_ extract 31 24) temp320)))
(define-fun esp5 () (_ BitVec 32) (bvsub esp4 (_ bv4 32)))
(define-fun memory6 () (Array (_ BitVec 32) (_ BitVec 8)) (store (store (store (store memory5 (bvsub esp5 (_ bv4 32)) ((_ extract 7 0) ebp0)) (bvsub esp5 (_ bv3 32)) ((_ extract 15 8) ebp0)) (bvsub esp5 (_ bv2 32)) ((_ extract 23 16) ebp0)) (bvsub esp5 (_ bv1 32)) ((_ extract 31 24) ebp0)))
(define-fun esp6 () (_ BitVec 32) (bvsub esp5 (_ bv4 32)))
(define-fun memory7 () (Array (_ BitVec 32) (_ BitVec 8)) (store (store (store (store memory6 (bvsub esp6 (_ bv4 32)) ((_ extract 7 0) esi0)) (bvsub esp6 (_ bv3 32)) ((_ extract 15 8) esi0)) (bvsub esp6 (_ bv2 32)) ((_ extract 23 16) esi0)) (bvsub esp6 (_ bv1 32)) ((_ extract 31 24) esi0)))
(define-fun esp7 () (_ BitVec 32) (bvsub esp6 (_ bv4 32)))
(define-fun memory8 () (Array (_ BitVec 32) (_ BitVec 8)) (store (store (store (store memory7 (bvsub esp7 (_ bv4 32)) ((_ extract 7 0) edi0)) (bvsub esp7 (_ bv3 32)) ((_ extract 15 8) edi0)) (bvsub esp7 (_ bv2 32)) ((_ extract 23 16) edi0)) (bvsub esp7 (_ bv1 32)) ((_ extract 31 24) edi0)))
(define-fun esp8 () (_ BitVec 32) (bvsub esp7 (_ bv4 32)))
(define-fun esp9 () (_ BitVec 32) (bvsub esp8 (_ bv4 32)))
(define-fun memory9 () (Array (_ BitVec 32) (_ BitVec 8)) (store (store (store (store memory8 esp9 (_ bv7 8)) (bvadd esp9 (_ bv1 32)) (_ bv80 8)) (bvadd esp9 (_ bv2 32)) (_ bv0 8)) (bvadd esp9 (_ bv3 32)) (_ bv1 8)))
(assert (= eax0 (_ bv0 32)))
(assert (= ebx0 (_ bv0 32)))
(assert (= ecx0 (_ bv0 32)))
(assert (= edx0 (_ bv0 32)))
(assert (= edi0 (_ bv0 32)))
(assert (= esi0 (_ bv0 32)))
(assert (= esp0 (_ bv458752 32)))
(assert (= ebp0 (_ bv458752 32)))
(check-sat)
(reset)



(set-option :produce-models true)
(set-logic QF_ABV)
(declare-fun memory0 () (Array (_ BitVec 32) (_ BitVec 8)))
(declare-fun eax0 () (_ BitVec 32))
(declare-fun ebx0 () (_ BitVec 32))
(declare-fun ecx0 () (_ BitVec 32))
(declare-fun edx0 () (_ BitVec 32))
(declare-fun esi0 () (_ BitVec 32))
(declare-fun edi0 () (_ BitVec 32))
(declare-fun ebp0 () (_ BitVec 32))
(declare-fun esp0 () (_ BitVec 32))
(declare-fun OF0 () (_ BitVec 1))
(declare-fun SF0 () (_ BitVec 1))
(declare-fun ZF0 () (_ BitVec 1))
(declare-fun PF0 () (_ BitVec 1))
(declare-fun CF0 () (_ BitVec 1))
(declare-fun AF0 () (_ BitVec 1))
(declare-fun DF0 () (_ BitVec 1))
(declare-fun fs_base0 () (_ BitVec 32))
(define-fun temp320 () (_ BitVec 32) esp0)
(define-fun memory1 () (Array (_ BitVec 32) (_ BitVec 8)) (store (store (store (store memory0 (bvsub esp0 (_ bv4 32)) ((_ extract 7 0) eax0)) (bvsub esp0 (_ bv3 32)) ((_ extract 15 8) eax0)) (bvsub esp0 (_ bv2 32)) ((_ extract 23 16) eax0)) (bvsub esp0 (_ bv1 32)) ((_ extract 31 24) eax0)))
(define-fun esp1 () (_ BitVec 32) (bvsub esp0 (_ bv4 32)))
(define-fun memory2 () (Array (_ BitVec 32) (_ BitVec 8)) (store (store (store (store memory1 (bvsub esp1 (_ bv4 32)) ((_ extract 7 0) ecx0)) (bvsub esp1 (_ bv3 32)) ((_ extract 15 8) ecx0)) (bvsub esp1 (_ bv2 32)) ((_ extract 23 16) ecx0)) (bvsub esp1 (_ bv1 32)) ((_ extract 31 24) ecx0)))
(define-fun esp2 () (_ BitVec 32) (bvsub esp1 (_ bv4 32)))
(define-fun memory3 () (Array (_ BitVec 32) (_ BitVec 8)) (store (store (store (store memory2 (bvsub esp2 (_ bv4 32)) ((_ extract 7 0) edx0)) (bvsub esp2 (_ bv3 32)) ((_ extract 15 8) edx0)) (bvsub esp2 (_ bv2 32)) ((_ extract 23 16) edx0)) (bvsub esp2 (_ bv1 32)) ((_ extract 31 24) edx0)))
(define-fun esp3 () (_ BitVec 32) (bvsub esp2 (_ bv4 32)))
(define-fun memory4 () (Array (_ BitVec 32) (_ BitVec 8)) (store (store (store (store memory3 (bvsub esp3 (_ bv4 32)) ((_ extract 7 0) ebx0)) (bvsub esp3 (_ bv3 32)) ((_ extract 15 8) ebx0)) (bvsub esp3 (_ bv2 32)) ((_ extract 23 16) ebx0)) (bvsub esp3 (_ bv1 32)) ((_ extract 31 24) ebx0)))
(define-fun esp4 () (_ BitVec 32) (bvsub esp3 (_ bv4 32)))
(define-fun memory5 () (Array (_ BitVec 32) (_ BitVec 8)) (store (store (store (store memory4 (bvsub esp4 (_ bv4 32)) ((_ extract 7 0) temp320)) (bvsub esp4 (_ bv3 32)) ((_ extract 15 8) temp320)) (bvsub esp4 (_ bv2 32)) ((_ extract 23 16) temp320)) (bvsub esp4 (_ bv1 32)) ((_ extract 31 24) temp320)))
(define-fun esp5 () (_ BitVec 32) (bvsub esp4 (_ bv4 32)))
(define-fun memory6 () (Array (_ BitVec 32) (_ BitVec 8)) (store (store (store (store memory5 (bvsub esp5 (_ bv4 32)) ((_ extract 7 0) ebp0)) (bvsub esp5 (_ bv3 32)) ((_ extract 15 8) ebp0)) (bvsub esp5 (_ bv2 32)) ((_ extract 23 16) ebp0)) (bvsub esp5 (_ bv1 32)) ((_ extract 31 24) ebp0)))
(define-fun esp6 () (_ BitVec 32) (bvsub esp5 (_ bv4 32)))
(define-fun memory7 () (Array (_ BitVec 32) (_ BitVec 8)) (store (store (store (store memory6 (bvsub esp6 (_ bv4 32)) ((_ extract 7 0) esi0)) (bvsub esp6 (_ bv3 32)) ((_ extract 15 8) esi0)) (bvsub esp6 (_ bv2 32)) ((_ extract 23 16) esi0)) (bvsub esp6 (_ bv1 32)) ((_ extract 31 24) esi0)))
(define-fun esp7 () (_ BitVec 32) (bvsub esp6 (_ bv4 32)))
(define-fun memory8 () (Array (_ BitVec 32) (_ BitVec 8)) (store (store (store (store memory7 (bvsub esp7 (_ bv4 32)) ((_ extract 7 0) edi0)) (bvsub esp7 (_ bv3 32)) ((_ extract 15 8) edi0)) (bvsub esp7 (_ bv2 32)) ((_ extract 23 16) edi0)) (bvsub esp7 (_ bv1 32)) ((_ extract 31 24) edi0)))
(define-fun esp8 () (_ BitVec 32) (bvsub esp7 (_ bv4 32)))
(define-fun esp9 () (_ BitVec 32) (bvsub esp8 (_ bv4 32)))
(define-fun memory9 () (Array (_ BitVec 32) (_ BitVec 8)) (store (store (store (store memory8 esp9 (_ bv7 8)) (bvadd esp9 (_ bv1 32)) (_ bv80 8)) (bvadd esp9 (_ bv2 32)) (_ bv0 8)) (bvadd esp9 (_ bv3 32)) (_ bv1 8)))
(assert (= eax0 (_ bv0 32)))
(assert (= ebx0 (_ bv0 32)))
(assert (= ecx0 (_ bv0 32)))
(assert (= edx0 (_ bv0 32)))
(assert (= edi0 (_ bv0 32)))
(assert (= esi0 (_ bv0 32)))
(assert (= esp0 (_ bv458752 32)))
(assert (= ebp0 (_ bv458752 32)))
(check-sat)
(reset)



(set-option :produce-models true)
(set-logic QF_ABV)
(declare-fun memory0 () (Array (_ BitVec 32) (_ BitVec 8)))
(declare-fun eax0 () (_ BitVec 32))
(declare-fun ebx0 () (_ BitVec 32))
(declare-fun ecx0 () (_ BitVec 32))
(declare-fun edx0 () (_ BitVec 32))
(declare-fun esi0 () (_ BitVec 32))
(declare-fun edi0 () (_ BitVec 32))
(declare-fun ebp0 () (_ BitVec 32))
(declare-fun esp0 () (_ BitVec 32))
(declare-fun OF0 () (_ BitVec 1))
(declare-fun SF0 () (_ BitVec 1))
(declare-fun ZF0 () (_ BitVec 1))
(declare-fun PF0 () (_ BitVec 1))
(declare-fun CF0 () (_ BitVec 1))
(declare-fun AF0 () (_ BitVec 1))
(declare-fun DF0 () (_ BitVec 1))
(declare-fun fs_base0 () (_ BitVec 32))
(define-fun temp320 () (_ BitVec 32) esp0)
(define-fun memory1 () (Array (_ BitVec 32) (_ BitVec 8)) (store (store (store (store memory0 (bvsub esp0 (_ bv4 32)) ((_ extract 7 0) eax0)) (bvsub esp0 (_ bv3 32)) ((_ extract 15 8) eax0)) (bvsub esp0 (_ bv2 32)) ((_ extract 23 16) eax0)) (bvsub esp0 (_ bv1 32)) ((_ extract 31 24) eax0)))
(define-fun esp1 () (_ BitVec 32) (bvsub esp0 (_ bv4 32)))
(define-fun memory2 () (Array (_ BitVec 32) (_ BitVec 8)) (store (store (store (store memory1 (bvsub esp1 (_ bv4 32)) ((_ extract 7 0) ecx0)) (bvsub esp1 (_ bv3 32)) ((_ extract 15 8) ecx0)) (bvsub esp1 (_ bv2 32)) ((_ extract 23 16) ecx0)) (bvsub esp1 (_ bv1 32)) ((_ extract 31 24) ecx0)))
(define-fun esp2 () (_ BitVec 32) (bvsub esp1 (_ bv4 32)))
(define-fun memory3 () (Array (_ BitVec 32) (_ BitVec 8)) (store (store (store (store memory2 (bvsub esp2 (_ bv4 32)) ((_ extract 7 0) edx0)) (bvsub esp2 (_ bv3 32)) ((_ extract 15 8) edx0)) (bvsub esp2 (_ bv2 32)) ((_ extract 23 16) edx0)) (bvsub esp2 (_ bv1 32)) ((_ extract 31 24) edx0)))
(define-fun esp3 () (_ BitVec 32) (bvsub esp2 (_ bv4 32)))
(define-fun memory4 () (Array (_ BitVec 32) (_ BitVec 8)) (store (store (store (store memory3 (bvsub esp3 (_ bv4 32)) ((_ extract 7 0) ebx0)) (bvsub esp3 (_ bv3 32)) ((_ extract 15 8) ebx0)) (bvsub esp3 (_ bv2 32)) ((_ extract 23 16) ebx0)) (bvsub esp3 (_ bv1 32)) ((_ extract 31 24) ebx0)))
(define-fun esp4 () (_ BitVec 32) (bvsub esp3 (_ bv4 32)))
(define-fun memory5 () (Array (_ BitVec 32) (_ BitVec 8)) (store (store (store (store memory4 (bvsub esp4 (_ bv4 32)) ((_ extract 7 0) temp320)) (bvsub esp4 (_ bv3 32)) ((_ extract 15 8) temp320)) (bvsub esp4 (_ bv2 32)) ((_ extract 23 16) temp320)) (bvsub esp4 (_ bv1 32)) ((_ extract 31 24) temp320)))
(define-fun esp5 () (_ BitVec 32) (bvsub esp4 (_ bv4 32)))
(define-fun memory6 () (Array (_ BitVec 32) (_ BitVec 8)) (store (store (store (store memory5 (bvsub esp5 (_ bv4 32)) ((_ extract 7 0) ebp0)) (bvsub esp5 (_ bv3 32)) ((_ extract 15 8) ebp0)) (bvsub esp5 (_ bv2 32)) ((_ extract 23 16) ebp0)) (bvsub esp5 (_ bv1 32)) ((_ extract 31 24) ebp0)))
(define-fun esp6 () (_ BitVec 32) (bvsub esp5 (_ bv4 32)))
(define-fun memory7 () (Array (_ BitVec 32) (_ BitVec 8)) (store (store (store (store memory6 (bvsub esp6 (_ bv4 32)) ((_ extract 7 0) esi0)) (bvsub esp6 (_ bv3 32)) ((_ extract 15 8) esi0)) (bvsub esp6 (_ bv2 32)) ((_ extract 23 16) esi0)) (bvsub esp6 (_ bv1 32)) ((_ extract 31 24) esi0)))
(define-fun esp7 () (_ BitVec 32) (bvsub esp6 (_ bv4 32)))
(define-fun memory8 () (Array (_ BitVec 32) (_ BitVec 8)) (store (store (store (store memory7 (bvsub esp7 (_ bv4 32)) ((_ extract 7 0) edi0)) (bvsub esp7 (_ bv3 32)) ((_ extract 15 8) edi0)) (bvsub esp7 (_ bv2 32)) ((_ extract 23 16) edi0)) (bvsub esp7 (_ bv1 32)) ((_ extract 31 24) edi0)))
(define-fun esp8 () (_ BitVec 32) (bvsub esp7 (_ bv4 32)))
(define-fun esp9 () (_ BitVec 32) (bvsub esp8 (_ bv4 32)))
(define-fun memory9 () (Array (_ BitVec 32) (_ BitVec 8)) (store (store (store (store memory8 esp9 (_ bv7 8)) (bvadd esp9 (_ bv1 32)) (_ bv80 8)) (bvadd esp9 (_ bv2 32)) (_ bv0 8)) (bvadd esp9 (_ bv3 32)) (_ bv1 8)))
(assert (= eax0 (_ bv0 32)))
(assert (= ebx0 (_ bv0 32)))
(assert (= ecx0 (_ bv0 32)))
(assert (= edx0 (_ bv0 32)))
(assert (= edi0 (_ bv0 32)))
(assert (= esi0 (_ bv0 32)))
(assert (= esp0 (_ bv458752 32)))
(assert (= ebp0 (_ bv458752 32)))
(check-sat)
(reset)


